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

let H be ZF-formula; :: thesis:
assume H / (x,y) in WFF ; :: thesis:
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:

end;

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

let H1, H2 be ZF-formula; :: thesis:
assume ( H1 / (x,y) in WFF & H2 / (x,y) in WFF ) ; :: thesis:
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:

end;

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

let H be ZF-formula; :: thesis:
let z be Variable; :: thesis:
assume H / (x,y) in WFF ; :: thesis:
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:

end;

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

let x1, x2 be Variable; :: thesis:
( 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:

end;