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 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] )
A2: ex y1, y2 being Variable st (x1 '=' x2) / x,y = y1 '=' y2 by Th167;
ex z1, z2 being Variable st (x1 'in' x2) / x,y = z1 'in' z2 by Th169;
hence ( S₁[x1 '=' x2] & S₁[x1 'in' x2] ) by A2, ZF_LANG:14; :: thesis: verum

end;

A3: 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:14;
'not' F = ('not' H) / x,y by Th170;
hence S₁[ 'not' H] by ZF_LANG:14; :: thesis: verum

end;

A4: 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:14;
F1 '&' F2 = (H1 '&' H2) / x,y by Lm1;
hence S₁[H1 '&' H2] by ZF_LANG:14; :: thesis: verum

end;

A5: 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:14;
( z <> x or z = x ) ;
then consider s being Variable such that
A6: ( ( s = z & z <> x ) or ( s = y & z = x ) ) ;
All s,F = (All z,H) / x,y by A6, Lm2;
hence S₁[ All z,H] by ZF_LANG:14; :: thesis: verum

end;

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