let y, x be Variable; :: thesis:
let H be ZF-formula; :: thesis:
defpred S₁[ ZF-formula] means ( not y in variables_in $1 implies ( ( x in Free $1 implies Free ($1 / x,y) = ((Free $1) \ {x}) \/ {y} ) & ( not x in Free $1 implies Free ($1 / x,y) = Free $1 ) ) );
A1: for x1, x2 being Variable holds
( S₁[x1 '=' x2] & S₁[x1 'in' x2] )

proof

let x1, x2 be Variable; :: thesis:
( ( x1 = x or x1 <> x ) & ( x2 = x or x2 <> x ) ) ;
then consider y1, y2 being Variable such that
A2: ( ( 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 ) ) ;
( (x1 '=' x2) / x,y = y1 '=' y2 & (x1 'in' x2) / x,y = y1 'in' y2 ) by A2, ZF_LANG1:166, ZF_LANG1:168;
then A3: ( Free ((x1 '=' x2) / x,y) = {y1,y2} & Free (x1 '=' x2) = {x1,x2} & Free ((x1 'in' x2) / x,y) = {y1,y2} & Free (x1 'in' x2) = {x1,x2} ) by ZF_LANG1:63, ZF_LANG1:64;
A4: ( variables_in (x1 '=' x2) = {x1,x2} & variables_in (x1 'in' x2) = {x1,x2} ) by ZF_LANG1:151, ZF_LANG1:152;
thus S₁[x1 '=' x2] :: thesis:

proof

assume not y in variables_in (x1 '=' x2) ; :: thesis:
thus ( x in Free (x1 '=' x2) implies Free ((x1 '=' x2) / x,y) = ((Free (x1 '=' x2)) \ {x}) \/ {y} ) :: thesis:

proof

assume A5: x in Free (x1 '=' x2) ; :: thesis:
thus Free ((x1 '=' x2) / x,y) c= ((Free (x1 '=' x2)) \ {x}) \/ {y} by Th1; :: according to XBOOLE_0:def 10 :: thesis:
let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in ((Free (x1 '=' x2)) \ {x}) \/ {y} ; :: thesis:
then ( a in (Free (x1 '=' x2)) \ {x} or a in {y} ) by XBOOLE_0:def 3;
then ( ( a in Free (x1 '=' x2) & not a in {x} ) or a in {y} ) by XBOOLE_0:def 5;
then ( ( ( a = x1 or a = x2 ) & a <> x ) or a = y ) by A3, TARSKI:def 1, TARSKI:def 2;
hence a in Free ((x1 '=' x2) / x,y) by A2, A3, A5, TARSKI:def 2; :: thesis:

end;

assume not x in Free (x1 '=' x2) ; :: thesis:
hence Free ((x1 '=' x2) / x,y) = Free (x1 '=' x2) by A3, A4, ZF_LANG1:196; :: thesis:

end;

assume not y in variables_in (x1 'in' x2) ; :: thesis:
thus ( x in Free (x1 'in' x2) implies Free ((x1 'in' x2) / x,y) = ((Free (x1 'in' x2)) \ {x}) \/ {y} ) :: thesis:

proof

assume A6: x in Free (x1 'in' x2) ; :: thesis:
thus Free ((x1 'in' x2) / x,y) c= ((Free (x1 'in' x2)) \ {x}) \/ {y} by Th1; :: according to XBOOLE_0:def 10 :: thesis:
let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in ((Free (x1 'in' x2)) \ {x}) \/ {y} ; :: thesis:
then ( a in (Free (x1 'in' x2)) \ {x} or a in {y} ) by XBOOLE_0:def 3;
then ( ( a in Free (x1 'in' x2) & not a in {x} ) or a in {y} ) by XBOOLE_0:def 5;
then ( ( ( a = x1 or a = x2 ) & a <> x ) or a = y ) by A3, TARSKI:def 1, TARSKI:def 2;
hence a in Free ((x1 'in' x2) / x,y) by A2, A3, A6, TARSKI:def 2; :: thesis:

end;

assume not x in Free (x1 'in' x2) ; :: thesis:
hence Free ((x1 'in' x2) / x,y) = Free (x1 'in' x2) by A3, A4, ZF_LANG1:196; :: thesis:

end;

A7: for H being ZF-formula st S₁[H] holds
S₁[ 'not' H]

proof

let H be ZF-formula; :: thesis:
( Free ('not' (H / x,y)) = Free (H / x,y) & Free ('not' H) = Free H & variables_in ('not' H) = variables_in H & ('not' H) / x,y = 'not' (H / x,y) ) by ZF_LANG1:65, ZF_LANG1:153, ZF_LANG1:170;
hence ( S₁[H] implies S₁[ 'not' H] ) ; :: thesis:

end;

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

proof

let H1, H2 be ZF-formula; :: thesis:
assume that
A9: ( S₁[H1] & S₁[H2] ) and
A10: not y in variables_in (H1 '&' H2) ; :: thesis:
A11: ( Free (H1 '&' H2) = (Free H1) \/ (Free H2) & Free ((H1 / x,y) '&' (H2 / x,y)) = (Free (H1 / x,y)) \/ (Free (H2 / x,y)) & variables_in (H1 '&' H2) = (variables_in H1) \/ (variables_in H2) ) by ZF_LANG1:66, ZF_LANG1:154;
set H = H1 '&' H2;
A12: (H1 '&' H2) / x,y = (H1 / x,y) '&' (H2 / x,y) by ZF_LANG1:172;
thus ( x in Free (H1 '&' H2) implies Free ((H1 '&' H2) / x,y) = ((Free (H1 '&' H2)) \ {x}) \/ {y} ) :: thesis:

proof

assume A13: x in Free (H1 '&' H2) ; :: thesis:

A14: now

assume not x in Free H1 ; :: thesis:
then ( x in Free H2 & Free (H1 / x,y) = Free H1 & Free H1 = (Free H1) \ {x} ) by A9, A10, A11, A13, XBOOLE_0:def 3, ZFMISC_1:65;
hence Free ((H1 '&' H2) / x,y) = (((Free H1) \ {x}) \/ ((Free H2) \ {x})) \/ {y} by A9, A10, A11, A12, XBOOLE_0:def 3, XBOOLE_1:4
.= ((Free (H1 '&' H2)) \ {x}) \/ {y} by A11, XBOOLE_1:42 ;
:: thesis:

end;

A15: now

assume not x in Free H2 ; :: thesis:
then ( x in Free H1 & Free (H2 / x,y) = Free H2 & Free H2 = (Free H2) \ {x} ) by A9, A10, A11, A13, XBOOLE_0:def 3, ZFMISC_1:65;
hence Free ((H1 '&' H2) / x,y) = (((Free H1) \ {x}) \/ ((Free H2) \ {x})) \/ {y} by A9, A10, A11, A12, XBOOLE_0:def 3, XBOOLE_1:4
.= ((Free (H1 '&' H2)) \ {x}) \/ {y} by A11, XBOOLE_1:42 ;
:: thesis:

end;

now

assume ( x in Free H1 & x in Free H2 ) ; :: thesis:
hence Free ((H1 '&' H2) / x,y) = (({y} \/ ((Free H1) \ {x})) \/ ((Free H2) \ {x})) \/ {y} by A9, A10, A11, A12, XBOOLE_0:def 3, XBOOLE_1:4
.= ({y} \/ (((Free H1) \ {x}) \/ ((Free H2) \ {x}))) \/ {y} by XBOOLE_1:4
.= (((Free (H1 '&' H2)) \ {x}) \/ {y}) \/ {y} by A11, XBOOLE_1:42
.= ((Free (H1 '&' H2)) \ {x}) \/ ({y} \/ {y}) by XBOOLE_1:4
.= ((Free (H1 '&' H2)) \ {x}) \/ {y} ;
:: thesis:

end;

hence Free ((H1 '&' H2) / x,y) = ((Free (H1 '&' H2)) \ {x}) \/ {y} by A14, A15; :: thesis:

end;

assume not x in Free (H1 '&' H2) ; :: thesis:
hence Free ((H1 '&' H2) / x,y) = Free (H1 '&' H2) by A9, A10, A11, XBOOLE_0:def 3, ZF_LANG1:172; :: thesis:

end;

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

proof

let H be ZF-formula; :: thesis:
let z be Variable; :: thesis:
( z = x or z <> x ) ;
then consider s being Variable such that
A17: ( ( z = x & s = y ) or ( z <> x & s = z ) ) ;
assume that
A18: S₁[H] and
A19: not y in variables_in (All z,H) ; :: thesis:
set G = (All z,H) / x,y;
A20: ( Free (All z,H) = (Free H) \ {z} & Free (All s,(H / x,y)) = (Free (H / x,y)) \ {s} & variables_in (All z,H) = (variables_in H) \/ {z} ) by ZF_LANG1:67, ZF_LANG1:155;
then ( not y in variables_in H & not y in {z} ) by A19, XBOOLE_0:def 3;
then A21: ( y <> z & (All z,H) / x,y = All s,(H / x,y) ) by A17, TARSKI:def 1, ZF_LANG1:173, ZF_LANG1:174;
thus ( x in Free (All z,H) implies Free ((All z,H) / x,y) = ((Free (All z,H)) \ {x}) \/ {y} ) :: thesis:

proof

assume x in Free (All z,H) ; :: thesis:
then A22: ( x in Free H & not x in {z} ) by A20, XBOOLE_0:def 5;
thus Free ((All z,H) / x,y) c= ((Free (All z,H)) \ {x}) \/ {y} :: according to XBOOLE_0:def 10 :: thesis:

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in Free ((All z,H) / x,y) ; :: thesis:
then A23: ( a in ((Free H) \ {x}) \/ {y} & not a in {z} ) by A17, A18, A19, A20, A21, A22, TARSKI:def 1, XBOOLE_0:def 3, XBOOLE_0:def 5;
then ( a in (Free H) \ {x} or a in {y} ) by XBOOLE_0:def 3;
then ( ( a in Free H & not a in {x} ) or a in {y} ) by XBOOLE_0:def 5;
then ( ( a in Free (All z,H) & not a in {x} ) or a in {y} ) by A20, A23, XBOOLE_0:def 5;
then ( a in (Free (All z,H)) \ {x} or a in {y} ) by XBOOLE_0:def 5;
hence a in ((Free (All z,H)) \ {x}) \/ {y} by XBOOLE_0:def 3; :: thesis:

end;

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in ((Free (All z,H)) \ {x}) \/ {y} ; :: thesis:
then ( a in (Free (All z,H)) \ {x} or a in {y} ) by XBOOLE_0:def 3;
then ( ( a in Free (All z,H) & not a in {x} ) or ( a in {y} & a = y ) ) by TARSKI:def 1, XBOOLE_0:def 5;
then ( ( ( a in Free H & not a in {x} ) or a in {y} ) & not a in {z} ) by A19, A20, XBOOLE_0:def 3, XBOOLE_0:def 5;
then ( ( a in (Free H) \ {x} or a in {y} ) & not a in {z} ) by XBOOLE_0:def 5;
then ( a in ((Free H) \ {x}) \/ {y} & not a in {z} ) by XBOOLE_0:def 3;
hence a in Free ((All z,H) / x,y) by A17, A18, A19, A20, A21, A22, TARSKI:def 1, XBOOLE_0:def 3, XBOOLE_0:def 5; :: thesis:

end;

assume not x in Free (All z,H) ; :: thesis:
then A24: ( not x in Free H or x in {z} ) by A20, XBOOLE_0:def 5;
A25: Free (All z,H) c= variables_in (All z,H) by ZF_LANG1:164;

A26: now

assume A27: x in Free H ; :: thesis:
thus Free ((All z,H) / x,y) = Free (All z,H) :: thesis:

proof

thus Free ((All z,H) / x,y) c= Free (All z,H) :: according to XBOOLE_0:def 10 :: thesis:

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume a in Free ((All z,H) / x,y) ; :: thesis:
then ( a in ((Free H) \ {z}) \/ {y} & not a in {y} ) by A17, A18, A19, A20, A21, A24, A27, TARSKI:def 1, XBOOLE_0:def 3, XBOOLE_0:def 5;
hence a in Free (All z,H) by A20, XBOOLE_0:def 3; :: thesis:

end;

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume A28: a in Free (All z,H) ; :: thesis:
then A29: ( a in ((Free H) \ {x}) \/ {y} & a in variables_in (All z,H) ) by A17, A20, A24, A25, A27, TARSKI:def 1, XBOOLE_0:def 3;
a <> y by A19, A25, A28;
then not a in {y} by TARSKI:def 1;
hence a in Free ((All z,H) / x,y) by A17, A18, A19, A20, A21, A24, A27, A29, TARSKI:def 1, XBOOLE_0:def 3, XBOOLE_0:def 5; :: thesis:

end;

now

assume not x in Free H ; :: thesis:
then ( ( Free ((All z,H) / x,y) = ((Free H) \ {z}) \ {y} & not y in Free (All z,H) ) or Free ((All z,H) / x,y) = (Free H) \ {z} ) by A17, A18, A19, A20, A21, A25, XBOOLE_0:def 3, ZFMISC_1:65;
hence Free ((All z,H) / x,y) = Free (All z,H) by A20, ZFMISC_1:65; :: thesis:

end;

hence Free ((All z,H) / x,y) = Free (All z,H) by A26; :: thesis:

end;

for H being ZF-formula holds S₁[H] from ZF_LANG1:sch 1(A1, A7, A8, A16);
hence ( not y in variables_in H implies ( ( x in Free H implies Free (H / x,y) = ((Free H) \ {x}) \/ {y} ) & ( not x in Free H implies Free (H / x,y) = Free H ) ) ) ; :: thesis: