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 H1, H2 being ZF-formula st S₁[H1] & S₁[H2] holds
S₁[H1 '&' H2]

proof

let H1, H2 be ZF-formula; :: thesis:
assume that
A2: S₁[H1] and
A3: S₁[H2] and
A4: not y in variables_in (H1 '&' H2) ; :: thesis:
A5: Free ((H1 / x,y) '&' (H2 / x,y)) = (Free (H1 / x,y)) \/ (Free (H2 / x,y)) by ZF_LANG1:66;
set H = H1 '&' H2;
A6: Free (H1 '&' H2) = (Free H1) \/ (Free H2) by ZF_LANG1:66;
A7: variables_in (H1 '&' H2) = (variables_in H1) \/ (variables_in H2) by ZF_LANG1:154;
A8: (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 A9: x in Free (H1 '&' H2) ; :: thesis:

A10: now

assume A11: not x in Free H1 ; :: thesis:
then Free H1 = (Free H1) \ {x} by ZFMISC_1:65;
hence Free ((H1 '&' H2) / x,y) = (((Free H1) \ {x}) \/ ((Free H2) \ {x})) \/ {y} by A2, A3, A4, A6, A5, A7, A8, A9, A11, XBOOLE_0:def 3, XBOOLE_1:4
.= ((Free (H1 '&' H2)) \ {x}) \/ {y} by A6, XBOOLE_1:42 ;
:: thesis:

end;

A12: now

assume A13: not x in Free H2 ; :: thesis:
then Free H2 = (Free H2) \ {x} by ZFMISC_1:65;
hence Free ((H1 '&' H2) / x,y) = (((Free H1) \ {x}) \/ ((Free H2) \ {x})) \/ {y} by A2, A3, A4, A6, A5, A7, A8, A9, A13, XBOOLE_0:def 3, XBOOLE_1:4
.= ((Free (H1 '&' H2)) \ {x}) \/ {y} by A6, XBOOLE_1:42 ;
:: thesis:

end;

now

assume that
A14: x in Free H1 and
A15: x in Free H2 ; :: thesis:
thus Free ((H1 '&' H2) / x,y) = (({y} \/ ((Free H1) \ {x})) \/ ((Free H2) \ {x})) \/ {y} by A2, A3, A4, A5, A7, A8, A14, A15, 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 A6, 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 A10, A12; :: thesis:

end;

assume not x in Free (H1 '&' H2) ; :: thesis:
hence Free ((H1 '&' H2) / x,y) = Free (H1 '&' H2) by A2, A3, A4, A6, A5, A7, 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:
assume that
A17: S₁[H] and
A18: not y in variables_in (All z,H) ; :: thesis:
set G = (All z,H) / x,y;
A19: Free (All z,H) = (Free H) \ {z} by ZF_LANG1:67;
( z = x or z <> x ) ;
then consider s being Variable such that
A20: ( ( z = x & s = y ) or ( z <> x & s = z ) ) ;
A21: (All z,H) / x,y = All s,(H / x,y) by A20, ZF_LANG1:173, ZF_LANG1:174;
A22: Free (All s,(H / x,y)) = (Free (H / x,y)) \ {s} by ZF_LANG1:67;
A23: variables_in (All z,H) = (variables_in H) \/ {z} by ZF_LANG1:155;
thus ( x in Free (All z,H) implies Free ((All z,H) / x,y) = ((Free (All z,H)) \ {x}) \/ {y} ) :: thesis:

proof

assume A24: x in Free (All z,H) ; :: thesis:
then A25: not x in {z} by A19, 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 A26: a in Free ((All z,H) / x,y) ; :: thesis:
then a in ((Free H) \ {x}) \/ {y} by A17, A18, A19, A22, A23, A21, A24, XBOOLE_0:def 3, XBOOLE_0:def 5;
then ( a in (Free H) \ {x} or a in {y} ) by XBOOLE_0:def 3;
then A27: ( ( a in Free H & not a in {x} ) or a in {y} ) by XBOOLE_0:def 5;
not a in {z} by A20, A22, A21, A25, A26, TARSKI:def 1, XBOOLE_0:def 5;
then ( ( a in Free (All z,H) & not a in {x} ) or a in {y} ) by A19, A27, 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 A28: ( ( 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} ) by A19, XBOOLE_0:def 5;
then ( a in (Free H) \ {x} or a in {y} ) by XBOOLE_0:def 5;
then A29: a in ((Free H) \ {x}) \/ {y} by XBOOLE_0:def 3;
not a in {z} by A18, A19, A23, A28, XBOOLE_0:def 3, XBOOLE_0:def 5;
hence a in Free ((All z,H) / x,y) by A20, A17, A18, A19, A22, A23, A21, A24, A25, A29, TARSKI:def 1, XBOOLE_0:def 3, XBOOLE_0:def 5; :: thesis:

end;

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

A32: now

assume A33: 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 A34: a in Free ((All z,H) / x,y) ; :: thesis:
then A35: not a in {y} by A20, A22, A21, A30, A33, TARSKI:def 1, XBOOLE_0:def 5;
a in ((Free H) \ {z}) \/ {y} by A20, A17, A18, A22, A23, A21, A30, A33, A34, TARSKI:def 1, XBOOLE_0:def 3, XBOOLE_0:def 5;
hence a in Free (All z,H) by A19, A35, XBOOLE_0:def 3; :: thesis:

end;

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume A36: a in Free (All z,H) ; :: thesis:
then a <> y by A18, A31;
then A37: not a in {y} by TARSKI:def 1;
a in ((Free H) \ {x}) \/ {y} by A20, A19, A30, A33, A36, TARSKI:def 1, XBOOLE_0:def 3;
hence a in Free ((All z,H) / x,y) by A20, A17, A18, A22, A23, A21, A30, A33, A37, 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 A20, A17, A18, A22, A23, A21, A31, XBOOLE_0:def 3, ZFMISC_1:65;
hence Free ((All z,H) / x,y) = Free (All z,H) by A19, ZFMISC_1:65; :: thesis:

end;

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

end;

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

proof

let x1, x2 be Variable; :: thesis:
A39: ( x2 = x or x2 <> x ) ;
( x1 = x or x1 <> x ) ;
then consider y1, y2 being Variable such that
A40: ( ( 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 A39;
(x1 '=' x2) / x,y = y1 '=' y2 by A40, ZF_LANG1:166;
then A41: Free ((x1 '=' x2) / x,y) = {y1,y2} by ZF_LANG1:63;
A42: Free (x1 '=' x2) = {x1,x2} by ZF_LANG1:63;
A43: variables_in (x1 '=' x2) = {x1,x2} by ZF_LANG1:151;
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 A44: 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 A42, TARSKI:def 1, TARSKI:def 2;
hence a in Free ((x1 '=' x2) / x,y) by A40, A41, A42, A44, TARSKI:def 2; :: thesis:

end;

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

end;

A45: Free (x1 'in' x2) = {x1,x2} by ZF_LANG1:64;
assume not y in variables_in (x1 'in' x2) ; :: thesis:
(x1 'in' x2) / x,y = y1 'in' y2 by A40, ZF_LANG1:168;
then A46: Free ((x1 'in' x2) / x,y) = {y1,y2} by ZF_LANG1:64;
thus ( x in Free (x1 'in' x2) implies Free ((x1 'in' x2) / x,y) = ((Free (x1 'in' x2)) \ {x}) \/ {y} ) :: thesis:

proof

assume A47: 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 A45, TARSKI:def 1, TARSKI:def 2;
hence a in Free ((x1 'in' x2) / x,y) by A40, A46, A45, A47, 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 A41, A42, A46, A45, A43, ZF_LANG1:196; :: thesis:

end;

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

proof

let H be ZF-formula; :: thesis:
A49: 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 A49, ZF_LANG1:153, ZF_LANG1:170; :: thesis:

end;

for H being ZF-formula holds S₁[H] from ZF_LANG1:sch 1(A38, A48, A1, 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: