let H be ZF-formula; for x, y being Variable holds H / (x,y) in WFF
let x, y be Variable; H / (x,y) in WFF
defpred S1[ ZF-formula] means $1 / (x,y) in WFF ;
A1:
for H being ZF-formula st S1[H] holds
S1[ 'not' H]
A2:
for H1, H2 being ZF-formula st S1[H1] & S1[H2] holds
S1[H1 '&' H2]
A3:
for H being ZF-formula
for z being Variable st S1[H] holds
S1[ All (z,H)]
proof
let H be
ZF-formula;
for z being Variable st S1[H] holds
S1[ All (z,H)]let z be
Variable;
( S1[H] implies S1[ All (z,H)] )
assume
H / (
x,
y)
in WFF
;
S1[ All (z,H)]
then reconsider F =
H / (
x,
y) as
ZF-formula by ZF_LANG:4;
(
z <> x or
z = x )
;
then consider s being
Variable such that A4:
( (
s = z &
z <> x ) or (
s = y &
z = x ) )
;
All (
s,
F)
= (All (z,H)) / (
x,
y)
by A4, Lm2;
hence
S1[
All (
z,
H)]
by ZF_LANG:4;
verum
end;
A5:
for x1, x2 being Variable holds
( S1[x1 '=' x2] & S1[x1 'in' x2] )
for H being ZF-formula holds S1[H]
from ZF_LANG1:sch 1(A5, A1, A2, A3);
hence
H / (x,y) in WFF
; verum