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_{1}[ ZF-formula] means Free ($1 / (x,y)) c= ((Free $1) \ {x}) \/ {y};

A1: for x1, x2 being Variable holds

( S_{1}[x1 '=' x2] & S_{1}[x1 'in' x2] )
_{1}[H1] & S_{1}[H2] holds

S_{1}[H1 '&' H2]

for z being Variable st S_{1}[H] holds

S_{1}[ All (z,H)]
_{1}[H] holds

S_{1}[ 'not' H]
_{1}[H]
from ZF_LANG1:sch 1(A1, A20, A6, A13);

hence Free (H / (x,y)) c= ((Free H) \ {x}) \/ {y} ; :: thesis: verum

let H be ZF-formula; :: thesis: Free (H / (x,y)) c= ((Free H) \ {x}) \/ {y}

defpred S

A1: for x1, x2 being Variable holds

( S

proof

A6:
for H1, H2 being ZF-formula st S
let x1, x2 be Variable; :: thesis: ( S_{1}[x1 '=' x2] & S_{1}[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}

then A5: Free ((x1 'in' x2) / (x,y)) = {y1,y2} by ZF_LANG1:59;

(x1 '=' x2) / (x,y) = y1 '=' y2 by A3, ZF_LANG1:152;

then Free ((x1 '=' x2) / (x,y)) = {y1,y2} by ZF_LANG1:58;

hence ( S_{1}[x1 '=' x2] & S_{1}[x1 'in' x2] )
by A5, A4, ZF_LANG1:58, ZF_LANG1:59; :: thesis: verum

end;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

(x1 'in' x2) / (x,y) = y1 'in' y2
by A3, ZF_LANG1:154;
let a be object ; :: 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;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

then A5: Free ((x1 'in' x2) / (x,y)) = {y1,y2} by ZF_LANG1:59;

(x1 '=' x2) / (x,y) = y1 '=' y2 by A3, ZF_LANG1:152;

then Free ((x1 '=' x2) / (x,y)) = {y1,y2} by ZF_LANG1:58;

hence ( S

S

proof

A13:
for H being ZF-formula
let H1, H2 be ZF-formula; :: thesis: ( S_{1}[H1] & S_{1}[H2] implies S_{1}[H1 '&' H2] )

assume that

A7: S_{1}[H1]
and

A8: S_{1}[H2]
; :: thesis: S_{1}[H1 '&' H2]

A9: Free ((H1 / (x,y)) '&' (H2 / (x,y))) = (Free (H1 / (x,y))) \/ (Free (H2 / (x,y))) by ZF_LANG1:61;

A10: (((Free H1) \ {x}) \/ {y}) \/ (((Free H2) \ {x}) \/ {y}) c= (((Free H1) \/ (Free H2)) \ {x}) \/ {y}

A12: Free (H1 '&' H2) = (Free H1) \/ (Free H2) by ZF_LANG1:61;

(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_{1}[H1 '&' H2]
by A9, A12, A11, A10, XBOOLE_1:1; :: thesis: verum

end;assume that

A7: S

A8: S

A9: Free ((H1 / (x,y)) '&' (H2 / (x,y))) = (Free (H1 / (x,y))) \/ (Free (H2 / (x,y))) by ZF_LANG1:61;

A10: (((Free H1) \ {x}) \/ {y}) \/ (((Free H2) \ {x}) \/ {y}) c= (((Free H1) \/ (Free H2)) \ {x}) \/ {y}

proof

A11:
(H1 '&' H2) / (x,y) = (H1 / (x,y)) '&' (H2 / (x,y))
by ZF_LANG1:158;
let a be object ; :: 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;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

A12: Free (H1 '&' H2) = (Free H1) \/ (Free H2) by ZF_LANG1:61;

(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

for z being Variable st S

S

proof

A20:
for H being ZF-formula st S
let H be ZF-formula; :: thesis: for z being Variable st S_{1}[H] holds

S_{1}[ All (z,H)]

let z be Variable; :: thesis: ( S_{1}[H] implies S_{1}[ All (z,H)] )

A14: Free (All (z,H)) = (Free H) \ {z} by ZF_LANG1:62;

( 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}_{1}[H]
; :: thesis: S_{1}[ 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:62;

(All (z,H)) / (x,y) = All (s,(H / (x,y))) by A15, ZF_LANG1:159, ZF_LANG1:160;

hence S_{1}[ All (z,H)]
by A19, A14, A18, A16, XBOOLE_1:1; :: thesis: verum

end;S

let z be Variable; :: thesis: ( S

A14: Free (All (z,H)) = (Free H) \ {z} by ZF_LANG1:62;

( 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

assume
S
let a be object ; :: 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 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

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:62;

(All (z,H)) / (x,y) = All (s,(H / (x,y))) by A15, ZF_LANG1:159, ZF_LANG1:160;

hence S

S

proof

for H being ZF-formula holds S
let H be ZF-formula; :: thesis: ( S_{1}[H] implies S_{1}[ 'not' H] )

A21: Free ('not' H) = Free H by ZF_LANG1:60;

Free ('not' (H / (x,y))) = Free (H / (x,y)) by ZF_LANG1:60;

hence ( S_{1}[H] implies S_{1}[ 'not' H] )
by A21, ZF_LANG1:156; :: thesis: verum

end;A21: Free ('not' H) = Free H by ZF_LANG1:60;

Free ('not' (H / (x,y))) = Free (H / (x,y)) by ZF_LANG1:60;

hence ( S

hence Free (H / (x,y)) c= ((Free H) \ {x}) \/ {y} ; :: thesis: verum