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 S1[ 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 S1[H1] & S1[H2] holds
S1[H1 '&' H2]
proof
let H1, H2 be ZF-formula; :: thesis: ( S1[H1] & S1[H2] implies S1[H1 '&' H2] )
assume that
A2: S1[H1] and
A3: S1[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) = () \/ () 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 A9: x in Free (H1 '&' H2) ; :: thesis: Free ((H1 '&' H2) / (x,y)) = ((Free (H1 '&' H2)) \ {x}) \/ {y}
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
.= ((Free (H1 '&' H2)) \ {x}) \/ {y} by ;
:: thesis: verum
end;
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
.= ((Free (H1 '&' H2)) \ {x}) \/ {y} by ;
:: thesis: verum
end;
now :: thesis: ( x in Free H1 & x in Free H2 implies Free ((H1 '&' H2) / (x,y)) = ((Free (H1 '&' H2)) \ {x}) \/ {y} )
assume 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
.= ({y} \/ (((Free H1) \ {x}) \/ ((Free H2) \ {x}))) \/ {y} by XBOOLE_1:4
.= (((Free (H1 '&' H2)) \ {x}) \/ {y}) \/ {y} by
.= ((Free (H1 '&' H2)) \ {x}) \/ ({y} \/ {y}) by XBOOLE_1:4
.= ((Free (H1 '&' H2)) \ {x}) \/ {y} ; :: thesis: verum
end;
hence Free ((H1 '&' H2) / (x,y)) = ((Free (H1 '&' H2)) \ {x}) \/ {y} by ; :: thesis: verum
end;
assume not x in Free (H1 '&' H2) ; :: thesis: Free ((H1 '&' H2) / (x,y)) = Free (H1 '&' H2)
hence Free ((H1 '&' H2) / (x,y)) = Free (H1 '&' H2) by ; :: thesis: verum
end;
A16: for H being ZF-formula
for z being Variable st S1[H] holds
S1[ All (z,H)]
proof
let H be ZF-formula; :: thesis: for z being Variable st S1[H] holds
S1[ All (z,H)]

let z be Variable; :: thesis: ( S1[H] implies S1[ All (z,H)] )
assume that
A17: S1[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 ;
A22: Free (All (s,(H / (x,y)))) = (Free (H / (x,y))) \ {s} by ZF_LANG1:62;
A23: variables_in (All (z,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 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 ;
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} )
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 ;
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 ;
then ( ( a in Free (All (z,H)) & not a in {x} ) or a in {y} ) by ;
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;
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 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 ;
then ( ( a in Free H & not a in {x} ) or a in {y} ) by ;
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 ;
hence a in Free ((All (z,H)) / (x,y)) by ; :: thesis: verum
end;
assume not x in Free (All (z,H)) ; :: thesis: Free ((All (z,H)) / (x,y)) = Free (All (z,H))
then A30: ( not x in Free H or x in {z} ) by ;
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
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))
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)) )
assume A34: a in Free ((All (z,H)) / (x,y)) ; :: thesis: a in Free (All (z,H))
then A35: not a in {y} by ;
a in ((Free H) \ {z}) \/ {y} by ;
hence a in Free (All (z,H)) by ; :: thesis: verum
end;
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)) )
assume A36: a in Free (All (z,H)) ; :: thesis: a in Free ((All (z,H)) / (x,y))
then a <> y by ;
then A37: not a in {y} by TARSKI:def 1;
a in ((Free H) \ {x}) \/ {y} by ;
hence a in Free ((All (z,H)) / (x,y)) by ; :: thesis: verum
end;
end;
now :: thesis: ( not x in Free H implies Free ((All (z,H)) / (x,y)) = Free (All (z,H)) )
assume 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 ;
hence Free ((All (z,H)) / (x,y)) = Free (All (z,H)) by ; :: thesis: verum
end;
hence Free ((All (z,H)) / (x,y)) = Free (All (z,H)) by A32; :: thesis: verum
end;
A38: for x1, x2 being Variable holds
( S1[x1 '=' x2] & S1[x1 'in' x2] )
proof
let x1, x2 be Variable; :: thesis: ( S1[x1 '=' x2] & S1[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 ;
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 S1[x1 '=' x2] :: thesis: S1[x1 'in' x2]
proof
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) )
proof
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 ;
hence a in Free ((x1 '=' x2) / (x,y)) by ; :: thesis: verum
end;
assume not x in Free (x1 '=' x2) ; :: thesis: Free ((x1 '=' x2) / (x,y)) = Free (x1 '=' x2)
hence Free ((x1 '=' x2) / (x,y)) = Free (x1 '=' x2) by ; :: thesis: verum
end;
A45: Free (x1 'in' x2) = {x1,x2} by ZF_LANG1:59;
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 ;
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 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 ;
hence a in Free ((x1 'in' x2) / (x,y)) by ; :: thesis: verum
end;
assume not x in Free (x1 'in' x2) ; :: thesis: Free ((x1 'in' x2) / (x,y)) = Free (x1 'in' x2)
hence Free ((x1 'in' x2) / (x,y)) = Free (x1 'in' x2) by ; :: thesis: verum
end;
A48: for H being ZF-formula st S1[H] holds
S1[ 'not' H]
proof
let H be ZF-formula; :: thesis: ( S1[H] implies S1[ 'not' H] )
A49: Free () = Free H by ZF_LANG1:60;
Free ('not' (H / (x,y))) = Free (H / (x,y)) by ZF_LANG1:60;
hence ( S1[H] implies S1[ 'not' H] ) by ; :: thesis: verum
end;
for H being ZF-formula holds S1[H] from 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