let x, y be Variable; :: thesis: for H being ZF-formula st not y in variables_in H holds

( ( 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 ) )

let H be ZF-formula; :: thesis: ( 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 ) ) )

defpred S_{1}[ 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_{1}[H1] & S_{1}[H2] holds

S_{1}[H1 '&' H2]

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

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

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

S_{1}[ 'not' H]
_{1}[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: verum

( ( 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 ) )

let H be ZF-formula; :: thesis: ( 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 ) ) )

defpred S

A1: for H1, H2 being ZF-formula st S

S

proof

A16:
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

A2: S_{1}[H1]
and

A3: S_{1}[H2]
and

A4: not y in variables_in (H1 '&' H2) ; :: thesis: ( ( x in Free (H1 '&' H2) implies Free ((H1 '&' H2) / (x,y)) = ((Free (H1 '&' H2)) \ {x}) \/ {y} ) & ( not x in Free (H1 '&' H2) implies Free ((H1 '&' H2) / (x,y)) = Free (H1 '&' H2) ) )

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

set H = H1 '&' H2;

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

A7: variables_in (H1 '&' H2) = (variables_in H1) \/ (variables_in H2) by ZF_LANG1:141;

A8: (H1 '&' H2) / (x,y) = (H1 / (x,y)) '&' (H2 / (x,y)) by ZF_LANG1:158;

thus ( x in Free (H1 '&' H2) implies Free ((H1 '&' H2) / (x,y)) = ((Free (H1 '&' H2)) \ {x}) \/ {y} ) :: thesis: ( not x in Free (H1 '&' H2) implies Free ((H1 '&' H2) / (x,y)) = Free (H1 '&' H2) )

hence Free ((H1 '&' H2) / (x,y)) = Free (H1 '&' H2) by A2, A3, A4, A6, A5, A7, XBOOLE_0:def 3, ZF_LANG1:158; :: thesis: verum

end;assume that

A2: S

A3: S

A4: not y in variables_in (H1 '&' H2) ; :: thesis: ( ( x in Free (H1 '&' H2) implies Free ((H1 '&' H2) / (x,y)) = ((Free (H1 '&' H2)) \ {x}) \/ {y} ) & ( not x in Free (H1 '&' H2) implies Free ((H1 '&' H2) / (x,y)) = Free (H1 '&' H2) ) )

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

set H = H1 '&' H2;

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

A7: variables_in (H1 '&' H2) = (variables_in H1) \/ (variables_in H2) by ZF_LANG1:141;

A8: (H1 '&' H2) / (x,y) = (H1 / (x,y)) '&' (H2 / (x,y)) by ZF_LANG1:158;

thus ( x in Free (H1 '&' H2) implies Free ((H1 '&' H2) / (x,y)) = ((Free (H1 '&' H2)) \ {x}) \/ {y} ) :: thesis: ( not x in Free (H1 '&' H2) implies Free ((H1 '&' H2) / (x,y)) = Free (H1 '&' H2) )

proof

assume
not x in Free (H1 '&' H2)
; :: thesis: Free ((H1 '&' H2) / (x,y)) = Free (H1 '&' H2)
assume A9:
x in Free (H1 '&' H2)
; :: thesis: Free ((H1 '&' H2) / (x,y)) = ((Free (H1 '&' H2)) \ {x}) \/ {y}

end;A10: now :: thesis: ( not x in Free H1 implies Free ((H1 '&' H2) / (x,y)) = ((Free (H1 '&' H2)) \ {x}) \/ {y} )

assume A11:
not x in Free H1
; :: thesis: Free ((H1 '&' H2) / (x,y)) = ((Free (H1 '&' H2)) \ {x}) \/ {y}

then Free H1 = (Free H1) \ {x} by ZFMISC_1:57;

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: verum

end;then Free H1 = (Free H1) \ {x} by ZFMISC_1:57;

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: verum

A12: now :: thesis: ( not x in Free H2 implies Free ((H1 '&' H2) / (x,y)) = ((Free (H1 '&' H2)) \ {x}) \/ {y} )

assume A13:
not x in Free H2
; :: thesis: Free ((H1 '&' H2) / (x,y)) = ((Free (H1 '&' H2)) \ {x}) \/ {y}

then Free H2 = (Free H2) \ {x} by ZFMISC_1:57;

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: verum

end;then Free H2 = (Free H2) \ {x} by ZFMISC_1:57;

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: verum

now :: thesis: ( x in Free H1 & x in Free H2 implies Free ((H1 '&' H2) / (x,y)) = ((Free (H1 '&' H2)) \ {x}) \/ {y} )

hence
Free ((H1 '&' H2) / (x,y)) = ((Free (H1 '&' H2)) \ {x}) \/ {y}
by A10, A12; :: thesis: verumassume that

A14: x in Free H1 and

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

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: verum

end;A14: x in Free H1 and

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

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: verum

hence Free ((H1 '&' H2) / (x,y)) = Free (H1 '&' H2) by A2, A3, A4, A6, A5, A7, XBOOLE_0:def 3, ZF_LANG1:158; :: thesis: verum

for z being Variable st S

S

proof

A38:
for x1, x2 being Variable holds
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)] )

assume that

A17: S_{1}[H]
and

A18: not y in variables_in (All (z,H)) ; :: thesis: ( ( x in Free (All (z,H)) implies Free ((All (z,H)) / (x,y)) = ((Free (All (z,H))) \ {x}) \/ {y} ) & ( not x in Free (All (z,H)) implies Free ((All (z,H)) / (x,y)) = Free (All (z,H)) ) )

set G = (All (z,H)) / (x,y);

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

( 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:159, ZF_LANG1:160;

A22: Free (All (s,(H / (x,y)))) = (Free (H / (x,y))) \ {s} by ZF_LANG1:62;

A23: variables_in (All (z,H)) = (variables_in H) \/ {z} by ZF_LANG1:142;

thus ( x in Free (All (z,H)) implies Free ((All (z,H)) / (x,y)) = ((Free (All (z,H))) \ {x}) \/ {y} ) :: thesis: ( not x in Free (All (z,H)) implies Free ((All (z,H)) / (x,y)) = Free (All (z,H)) )

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

end;S

let z be Variable; :: thesis: ( S

assume that

A17: S

A18: not y in variables_in (All (z,H)) ; :: thesis: ( ( x in Free (All (z,H)) implies Free ((All (z,H)) / (x,y)) = ((Free (All (z,H))) \ {x}) \/ {y} ) & ( not x in Free (All (z,H)) implies Free ((All (z,H)) / (x,y)) = Free (All (z,H)) ) )

set G = (All (z,H)) / (x,y);

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

( 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:159, ZF_LANG1:160;

A22: Free (All (s,(H / (x,y)))) = (Free (H / (x,y))) \ {s} by ZF_LANG1:62;

A23: variables_in (All (z,H)) = (variables_in H) \/ {z} by ZF_LANG1:142;

thus ( x in Free (All (z,H)) implies Free ((All (z,H)) / (x,y)) = ((Free (All (z,H))) \ {x}) \/ {y} ) :: thesis: ( not x in Free (All (z,H)) implies Free ((All (z,H)) / (x,y)) = Free (All (z,H)) )

proof

assume
not x in Free (All (z,H))
; :: thesis: Free ((All (z,H)) / (x,y)) = Free (All (z,H))
assume A24:
x in Free (All (z,H))
; :: thesis: Free ((All (z,H)) / (x,y)) = ((Free (All (z,H))) \ {x}) \/ {y}

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: ((Free (All (z,H))) \ {x}) \/ {y} c= Free ((All (z,H)) / (x,y))

assume a in ((Free (All (z,H))) \ {x}) \/ {y} ; :: thesis: a in Free ((All (z,H)) / (x,y))

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: verum

end;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: ((Free (All (z,H))) \ {x}) \/ {y} c= Free ((All (z,H)) / (x,y))

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in ((Free (All (z,H))) \ {x}) \/ {y} or a in Free ((All (z,H)) / (x,y)) )
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Free ((All (z,H)) / (x,y)) or a in ((Free (All (z,H))) \ {x}) \/ {y} )

assume A26: a in Free ((All (z,H)) / (x,y)) ; :: thesis: a in ((Free (All (z,H))) \ {x}) \/ {y}

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: verum

end;assume A26: a in Free ((All (z,H)) / (x,y)) ; :: thesis: a in ((Free (All (z,H))) \ {x}) \/ {y}

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: verum

assume a in ((Free (All (z,H))) \ {x}) \/ {y} ; :: thesis: a in Free ((All (z,H)) / (x,y))

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: verum

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

A32: now :: thesis: ( x in Free H implies Free ((All (z,H)) / (x,y)) = Free (All (z,H)) )

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

thus Free ((All (z,H)) / (x,y)) = Free (All (z,H)) :: thesis: verum

end;thus Free ((All (z,H)) / (x,y)) = Free (All (z,H)) :: thesis: verum

proof

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

assume A36: a in Free (All (z,H)) ; :: thesis: a in Free ((All (z,H)) / (x,y))

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: verum

end;proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Free (All (z,H)) or a in Free ((All (z,H)) / (x,y)) )
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Free ((All (z,H)) / (x,y)) or a in Free (All (z,H)) )

assume A34: a in Free ((All (z,H)) / (x,y)) ; :: thesis: a in Free (All (z,H))

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: verum

end;assume A34: a in Free ((All (z,H)) / (x,y)) ; :: thesis: a in Free (All (z,H))

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: verum

assume A36: a in Free (All (z,H)) ; :: thesis: a in Free ((All (z,H)) / (x,y))

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: verum

now :: thesis: ( not x in Free H implies Free ((All (z,H)) / (x,y)) = Free (All (z,H)) )

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

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

hence Free ((All (z,H)) / (x,y)) = Free (All (z,H)) by A19, ZFMISC_1:57; :: thesis: verum

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

hence Free ((All (z,H)) / (x,y)) = Free (All (z,H)) by A19, ZFMISC_1:57; :: thesis: verum

( S

proof

A48:
for H being ZF-formula st S
let x1, x2 be Variable; :: thesis: ( S_{1}[x1 '=' x2] & S_{1}[x1 'in' x2] )

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

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

A42: Free (x1 '=' x2) = {x1,x2} by ZF_LANG1:58;

A43: variables_in (x1 '=' x2) = {x1,x2} by ZF_LANG1:138;

thus S_{1}[x1 '=' x2]
:: thesis: S_{1}[x1 'in' x2]

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

(x1 'in' x2) / (x,y) = y1 'in' y2 by A40, ZF_LANG1:154;

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

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

hence Free ((x1 'in' x2) / (x,y)) = Free (x1 'in' x2) by A41, A42, A46, A45, A43, ZF_LANG1:182; :: thesis: verum

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

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

A42: Free (x1 '=' x2) = {x1,x2} by ZF_LANG1:58;

A43: variables_in (x1 '=' x2) = {x1,x2} by ZF_LANG1:138;

thus S

proof

A45:
Free (x1 'in' x2) = {x1,x2}
by ZF_LANG1:59;
assume
not y in variables_in (x1 '=' x2)
; :: thesis: ( ( x in Free (x1 '=' x2) implies Free ((x1 '=' x2) / (x,y)) = ((Free (x1 '=' x2)) \ {x}) \/ {y} ) & ( not x in Free (x1 '=' x2) implies Free ((x1 '=' x2) / (x,y)) = Free (x1 '=' x2) ) )

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

hence Free ((x1 '=' x2) / (x,y)) = Free (x1 '=' x2) by A42, A43, ZF_LANG1:182; :: thesis: verum

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

proof

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

thus Free ((x1 '=' x2) / (x,y)) c= ((Free (x1 '=' x2)) \ {x}) \/ {y} by Th1; :: according to XBOOLE_0:def 10 :: thesis: ((Free (x1 '=' x2)) \ {x}) \/ {y} c= Free ((x1 '=' x2) / (x,y))

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in ((Free (x1 '=' x2)) \ {x}) \/ {y} or a in Free ((x1 '=' x2) / (x,y)) )

assume a in ((Free (x1 '=' x2)) \ {x}) \/ {y} ; :: thesis: a in Free ((x1 '=' x2) / (x,y))

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: verum

end;thus Free ((x1 '=' x2) / (x,y)) c= ((Free (x1 '=' x2)) \ {x}) \/ {y} by Th1; :: according to XBOOLE_0:def 10 :: thesis: ((Free (x1 '=' x2)) \ {x}) \/ {y} c= Free ((x1 '=' x2) / (x,y))

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in ((Free (x1 '=' x2)) \ {x}) \/ {y} or a in Free ((x1 '=' x2) / (x,y)) )

assume a in ((Free (x1 '=' x2)) \ {x}) \/ {y} ; :: thesis: a in Free ((x1 '=' x2) / (x,y))

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: verum

hence Free ((x1 '=' x2) / (x,y)) = Free (x1 '=' x2) by A42, A43, ZF_LANG1:182; :: thesis: verum

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

(x1 'in' x2) / (x,y) = y1 'in' y2 by A40, ZF_LANG1:154;

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

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

proof

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

thus Free ((x1 'in' x2) / (x,y)) c= ((Free (x1 'in' x2)) \ {x}) \/ {y} by Th1; :: according to XBOOLE_0:def 10 :: thesis: ((Free (x1 'in' x2)) \ {x}) \/ {y} c= Free ((x1 'in' x2) / (x,y))

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in ((Free (x1 'in' x2)) \ {x}) \/ {y} or a in Free ((x1 'in' x2) / (x,y)) )

assume a in ((Free (x1 'in' x2)) \ {x}) \/ {y} ; :: thesis: a in Free ((x1 'in' x2) / (x,y))

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: verum

end;thus Free ((x1 'in' x2) / (x,y)) c= ((Free (x1 'in' x2)) \ {x}) \/ {y} by Th1; :: according to XBOOLE_0:def 10 :: thesis: ((Free (x1 'in' x2)) \ {x}) \/ {y} c= Free ((x1 'in' x2) / (x,y))

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in ((Free (x1 'in' x2)) \ {x}) \/ {y} or a in Free ((x1 'in' x2) / (x,y)) )

assume a in ((Free (x1 'in' x2)) \ {x}) \/ {y} ; :: thesis: a in Free ((x1 'in' x2) / (x,y))

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: verum

hence Free ((x1 'in' x2) / (x,y)) = Free (x1 'in' x2) by A41, A42, A46, A45, A43, ZF_LANG1:182; :: thesis: verum

S

proof

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

A49: 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 A49, ZF_LANG1:140, ZF_LANG1:156; :: thesis: verum

end;A49: 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 ( 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: verum