let H be ZF-formula; :: thesis: for x, y being Variable holds H / (x,y) in WFF
let x, y be Variable; :: thesis: H / (x,y) in WFF
defpred S₁[ ZF-formula] means $1 / (x,y) in WFF ;
A1: for H being ZF-formula st S₁[H] holds
S₁[ 'not' H]

proof

let H be ZF-formula; :: thesis: ( S₁[H] implies S₁[ 'not' H] )
assume H / (x,y) in WFF ; :: thesis: S₁[ 'not' H]
then reconsider F = H / (x,y) as ZF-formula by ZF_LANG:4;
'not' F = ('not' H) / (x,y) by Th156;
hence S₁[ 'not' H] by ZF_LANG:4; :: thesis: verum

end;

A2: for H1, H2 being ZF-formula st S₁[H1] & S₁[H2] holds
S₁[H1 '&' H2]

proof

let H1, H2 be ZF-formula; :: thesis: ( S₁[H1] & S₁[H2] implies S₁[H1 '&' H2] )
assume ( H1 / (x,y) in WFF & H2 / (x,y) in WFF ) ; :: thesis: S₁[H1 '&' H2]
then reconsider F1 = H1 / (x,y), F2 = H2 / (x,y) as ZF-formula by ZF_LANG:4;
F1 '&' F2 = (H1 '&' H2) / (x,y) by Lm1;
hence S₁[H1 '&' H2] by ZF_LANG:4; :: thesis: verum

end;

A3: for H being ZF-formula
for z being Variable st S₁[H] holds
S₁[ All (z,H)]

proof

let H be ZF-formula; :: thesis: for z being Variable st S₁[H] holds
S₁[ All (z,H)]
let z be Variable; :: thesis: ( S₁[H] implies S₁[ All (z,H)] )
assume H / (x,y) in WFF ; :: thesis: S₁[ 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 S₁[ All (z,H)] by ZF_LANG:4; :: thesis: verum

end;

A5: for x1, x2 being Variable holds
( S₁[x1 '=' x2] & S₁[x1 'in' x2] )

proof

let x1, x2 be Variable; :: thesis: ( S₁[x1 '=' x2] & S₁[x1 'in' x2] )
( ex y1, y2 being Variable st (x1 '=' x2) / (x,y) = y1 '=' y2 & ex z1, z2 being Variable st (x1 'in' x2) / (x,y) = z1 'in' z2 ) by Th153, Th155;
hence ( S₁[x1 '=' x2] & S₁[x1 'in' x2] ) by ZF_LANG:4; :: thesis: verum

end;

for H being ZF-formula holds S₁[H] from ZF_LANG1:sch 1(A5, A1, A2, A3);
hence H / (x,y) in WFF ; :: thesis: verum