let x, y be Variable; :: thesis: for H being ZF-formula holds Free (H / x,y) c= ((Free H) \ {x}) \/ {y}
let H be ZF-formula; :: thesis: Free (H / x,y) c= ((Free H) \ {x}) \/ {y}
defpred S₁[ ZF-formula] means Free ($1 / x,y) c= ((Free $1) \ {x}) \/ {y};
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: ( x2 = x or x2 <> x ) ;
( x1 = x or x1 <> x ) ;
then consider y1, y2 being Variable such that
A3: ( ( x1 <> x & x2 <> x & y1 = x1 & y2 = x2 ) or ( x1 = x & x2 <> x & y1 = y & y2 = x2 ) or ( x1 <> x & x2 = x & y1 = x1 & y2 = y ) or ( x1 = x & x2 = x & y1 = y & y2 = y ) ) by A2;
A4: {y1,y2} c= ({x1,x2} \ {x}) \/ {y}

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in {y1,y2} or a in ({x1,x2} \ {x}) \/ {y} )
assume a in {y1,y2} ; :: thesis: a in ({x1,x2} \ {x}) \/ {y}
then ( ( ( a = x1 or a = x2 ) & a <> x ) or a = y ) by A3, TARSKI:def 2;
then ( ( a in {x1,x2} & not a in {x} ) or a in {y} ) by TARSKI:def 1, TARSKI:def 2;
then ( a in {x1,x2} \ {x} or a in {y} ) by XBOOLE_0:def 5;
hence a in ({x1,x2} \ {x}) \/ {y} by XBOOLE_0:def 3; :: thesis: verum

end;

(x1 'in' x2) / x,y = y1 'in' y2 by A3, ZF_LANG1:168;
then A5: Free ((x1 'in' x2) / x,y) = {y1,y2} by ZF_LANG1:64;
(x1 '=' x2) / x,y = y1 '=' y2 by A3, ZF_LANG1:166;
then Free ((x1 '=' x2) / x,y) = {y1,y2} by ZF_LANG1:63;
hence ( S₁[x1 '=' x2] & S₁[x1 'in' x2] ) by A5, A4, ZF_LANG1:63, ZF_LANG1:64; :: thesis: verum

end;

A6: 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 that
A7: S₁[H1] and
A8: S₁[H2] ; :: thesis: S₁[H1 '&' H2]
A9: Free ((H1 / x,y) '&' (H2 / x,y)) = (Free (H1 / x,y)) \/ (Free (H2 / x,y)) by ZF_LANG1:66;
A10: (((Free H1) \ {x}) \/ {y}) \/ (((Free H2) \ {x}) \/ {y}) c= (((Free H1) \/ (Free H2)) \ {x}) \/ {y}

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (((Free H1) \ {x}) \/ {y}) \/ (((Free H2) \ {x}) \/ {y}) or a in (((Free H1) \/ (Free H2)) \ {x}) \/ {y} )
assume a in (((Free H1) \ {x}) \/ {y}) \/ (((Free H2) \ {x}) \/ {y}) ; :: thesis: a in (((Free H1) \/ (Free H2)) \ {x}) \/ {y}
then ( a in ((Free H1) \ {x}) \/ {y} or a in ((Free H2) \ {x}) \/ {y} ) by XBOOLE_0:def 3;
then ( a in (Free H1) \ {x} or a in (Free H2) \ {x} or a in {y} ) by XBOOLE_0:def 3;
then ( ( ( a in Free H1 or a in Free H2 ) & not a in {x} ) or a in {y} ) by XBOOLE_0:def 5;
then ( ( a in (Free H1) \/ (Free H2) & not a in {x} ) or a in {y} ) by XBOOLE_0:def 3;
then ( a in ((Free H1) \/ (Free H2)) \ {x} or a in {y} ) by XBOOLE_0:def 5;
hence a in (((Free H1) \/ (Free H2)) \ {x}) \/ {y} by XBOOLE_0:def 3; :: thesis: verum

end;

A11: (H1 '&' H2) / x,y = (H1 / x,y) '&' (H2 / x,y) by ZF_LANG1:172;
A12: Free (H1 '&' H2) = (Free H1) \/ (Free H2) by ZF_LANG1:66;
(Free (H1 / x,y)) \/ (Free (H2 / x,y)) c= (((Free H1) \ {x}) \/ {y}) \/ (((Free H2) \ {x}) \/ {y}) by A7, A8, XBOOLE_1:13;
hence S₁[H1 '&' H2] by A9, A12, A11, A10, XBOOLE_1:1; :: thesis: verum

end;

A13: 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] )
A14: Free (All z,H) = (Free H) \ {z} by ZF_LANG1:67;
( z = x or z <> x ) ;
then consider s being Variable such that
A15: ( ( z = x & s = y ) or ( z <> x & s = z ) ) ;
A16: (((Free H) \ {x}) \/ {y}) \ {s} c= (((Free H) \ {z}) \ {x}) \/ {y}

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (((Free H) \ {x}) \/ {y}) \ {s} or a in (((Free H) \ {z}) \ {x}) \/ {y} )
assume A17: a in (((Free H) \ {x}) \/ {y}) \ {s} ; :: thesis: a in (((Free H) \ {z}) \ {x}) \/ {y}
then ( a in (Free H) \ {x} or a in {y} ) by XBOOLE_0:def 3;
then ( ( a in Free H & not a in {z} & not a in {x} ) or a in {y} ) by A15, A17, XBOOLE_0:def 5;
then ( ( a in (Free H) \ {z} & not a in {x} ) or a in {y} ) by XBOOLE_0:def 5;
then ( a in ((Free H) \ {z}) \ {x} or a in {y} ) by XBOOLE_0:def 5;
hence a in (((Free H) \ {z}) \ {x}) \/ {y} by XBOOLE_0:def 3; :: thesis: verum

end;

assume S₁[H] ; :: thesis: S₁[ All z,H]
then A18: (Free (H / x,y)) \ {s} c= (((Free H) \ {x}) \/ {y}) \ {s} by XBOOLE_1:33;
A19: Free (All s,(H / x,y)) = (Free (H / x,y)) \ {s} by ZF_LANG1:67;
(All z,H) / x,y = All s,(H / x,y) by A15, ZF_LANG1:173, ZF_LANG1:174;
hence S₁[ All z,H] by A19, A14, A18, A16, XBOOLE_1:1; :: thesis: verum

end;

A20: 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] )
A21: Free ('not' H) = Free H by ZF_LANG1:65;
Free ('not' (H / x,y)) = Free (H / x,y) by ZF_LANG1:65;
hence ( S₁[H] implies S₁[ 'not' H] ) by A21, ZF_LANG1:170; :: thesis: verum

end;

for H being ZF-formula holds S₁[H] from ZF_LANG1:sch 1(A1, A20, A6, A13);
hence Free (H / x,y) c= ((Free H) \ {x}) \/ {y} ; :: thesis: verum