:: Replacing of Variables in Formulas of ZF Theory
:: by Grzegorz Bancerek
::
:: Received August 10, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

theorem Th1: :: ZF_LANG1:1
for x, y being Variable holds
( Var1 (x '=' y) = x & Var2 (x '=' y) = y )
proofend;

theorem Th2: :: ZF_LANG1:2
for x, y being Variable holds
( Var1 (x 'in' y) = x & Var2 (x 'in' y) = y )
proofend;

theorem Th3: :: ZF_LANG1:3
for p being ZF-formula holds the_argument_of ('not' p) = p
proofend;

theorem Th4: :: ZF_LANG1:4
for p, q being ZF-formula holds
( the_left_argument_of (p '&' q) = p & the_right_argument_of (p '&' q) = q )
proofend;

theorem :: ZF_LANG1:5
for p, q being ZF-formula holds
( the_left_argument_of (p 'or' q) = p & the_right_argument_of (p 'or' q) = q )
proofend;

theorem Th6: :: ZF_LANG1:6
for p, q being ZF-formula holds
( the_antecedent_of (p => q) = p & the_consequent_of (p => q) = q )
proofend;

theorem :: ZF_LANG1:7
for p, q being ZF-formula holds
( the_left_side_of (p <=> q) = p &amp; the_right_side_of (p <=> q) = q )
proofend;

theorem Th8: :: ZF_LANG1:8
for p being ZF-formula
for x being Variable holds
( bound_in (All (x,p)) = x &amp; the_scope_of (All (x,p)) = p )
proofend;

theorem Th9: :: ZF_LANG1:9
for p being ZF-formula
for x being Variable holds
( bound_in (Ex (x,p)) = x &amp; the_scope_of (Ex (x,p)) = p )
proofend;

theorem :: ZF_LANG1:10
for p, q being ZF-formula holds p 'or' q = ('not' p) => q ;

theorem :: ZF_LANG1:11
for p being ZF-formula
for x, y being Variable holds
( All (x,y,p) is universal &amp; bound_in (All (x,y,p)) = x &amp; the_scope_of (All (x,y,p)) = All (y,p) ) by Th8, ZF_LANG:5;

theorem :: ZF_LANG1:12
for p being ZF-formula
for x, y being Variable holds
( Ex (x,y,p) is existential &amp; bound_in (Ex (x,y,p)) = x &amp; the_scope_of (Ex (x,y,p)) = Ex (y,p) ) by Th9, ZF_LANG:6;

theorem :: ZF_LANG1:13
for p being ZF-formula
for x, y, z being Variable holds
( All (x,y,z,p) = All (x,(All (y,(All (z,p))))) &amp; All (x,y,z,p) = All (x,y,(All (z,p))) ) ;

theorem Th14: :: ZF_LANG1:14
for p1, p2 being ZF-formula
for x1, y1, x2, y2 being Variable st All (x1,y1,p1) = All (x2,y2,p2) holds
( x1 = x2 &amp; y1 = y2 &amp; p1 = p2 )
proofend;

theorem :: ZF_LANG1:15
for p1, p2 being ZF-formula
for x1, y1, z1, x2, y2, z2 being Variable st All (x1,y1,z1,p1) = All (x2,y2,z2,p2) holds
( x1 = x2 &amp; y1 = y2 &amp; z1 = z2 &amp; p1 = p2 )
proofend;

theorem :: ZF_LANG1:16
for p, q being ZF-formula
for x, y, z, t, s being Variable st All (x,y,z,p) = All (t,s,q) holds
( x = t &amp; y = s &amp; All (z,p) = q )
proofend;

theorem Th17: :: ZF_LANG1:17
for p1, p2 being ZF-formula
for x1, y1, x2, y2 being Variable st Ex (x1,y1,p1) = Ex (x2,y2,p2) holds
( x1 = x2 &amp; y1 = y2 &amp; p1 = p2 )
proofend;

theorem :: ZF_LANG1:18
for p being ZF-formula
for x, y, z being Variable holds
( Ex (x,y,z,p) = Ex (x,(Ex (y,(Ex (z,p))))) &amp; Ex (x,y,z,p) = Ex (x,y,(Ex (z,p))) ) ;

theorem :: ZF_LANG1:19
for p1, p2 being ZF-formula
for x1, y1, z1, x2, y2, z2 being Variable st Ex (x1,y1,z1,p1) = Ex (x2,y2,z2,p2) holds
( x1 = x2 &amp; y1 = y2 &amp; z1 = z2 &amp; p1 = p2 )
proofend;

theorem :: ZF_LANG1:20
for p, q being ZF-formula
for x, y, z, t, s being Variable st Ex (x,y,z,p) = Ex (t,s,q) holds
( x = t &amp; y = s &amp; Ex (z,p) = q )
proofend;

theorem :: ZF_LANG1:21
for p being ZF-formula
for x, y, z being Variable holds
( All (x,y,z,p) is universal &amp; bound_in (All (x,y,z,p)) = x &amp; the_scope_of (All (x,y,z,p)) = All (y,z,p) ) by Th8, ZF_LANG:5;

theorem :: ZF_LANG1:22
for p being ZF-formula
for x, y, z being Variable holds
( Ex (x,y,z,p) is existential &amp; bound_in (Ex (x,y,z,p)) = x &amp; the_scope_of (Ex (x,y,z,p)) = Ex (y,z,p) ) by Th9, ZF_LANG:6;

theorem :: ZF_LANG1:23
for H being ZF-formula st H is disjunctive holds
the_left_argument_of H = the_argument_of (the_left_argument_of (the_argument_of H))
proofend;

theorem :: ZF_LANG1:24
for H being ZF-formula st H is disjunctive holds
the_right_argument_of H = the_argument_of (the_right_argument_of (the_argument_of H))
proofend;

theorem :: ZF_LANG1:25
for H being ZF-formula st H is conditional holds
the_antecedent_of H = the_left_argument_of (the_argument_of H)
proofend;

theorem :: ZF_LANG1:26
for H being ZF-formula st H is conditional holds
the_consequent_of H = the_argument_of (the_right_argument_of (the_argument_of H))
proofend;

theorem :: ZF_LANG1:27
for H being ZF-formula st H is biconditional holds
( the_left_side_of H = the_antecedent_of (the_left_argument_of H) &amp; the_left_side_of H = the_consequent_of (the_right_argument_of H) )
proofend;

theorem :: ZF_LANG1:28
for H being ZF-formula st H is biconditional holds
( the_right_side_of H = the_consequent_of (the_left_argument_of H) &amp; the_right_side_of H = the_antecedent_of (the_right_argument_of H) )
proofend;

theorem :: ZF_LANG1:29
for H being ZF-formula st H is existential holds
( bound_in H = bound_in (the_argument_of H) &amp; the_scope_of H = the_argument_of (the_scope_of (the_argument_of H)) )
proofend;

theorem :: ZF_LANG1:30
for F, G being ZF-formula holds
( the_argument_of (F 'or' G) = ('not' F) '&amp;' ('not' G) &amp; the_antecedent_of (F 'or' G) = 'not' F &amp; the_consequent_of (F 'or' G) = G )
proofend;

theorem :: ZF_LANG1:31
for F, G being ZF-formula holds the_argument_of (F => G) = F '&amp;' ('not' G) by Th3;

theorem :: ZF_LANG1:32
for F, G being ZF-formula holds
( the_left_argument_of (F <=> G) = F => G &amp; the_right_argument_of (F <=> G) = G => F ) by Th4;

theorem :: ZF_LANG1:33
for H being ZF-formula
for x being Variable holds the_argument_of (Ex (x,H)) = All (x,('not' H)) by Th3;

theorem :: ZF_LANG1:34
for H being ZF-formula st H is disjunctive holds
( H is conditional &amp; H is negative &amp; the_argument_of H is conjunctive &amp; the_left_argument_of (the_argument_of H) is negative &amp; the_right_argument_of (the_argument_of H) is negative )
proofend;

theorem :: ZF_LANG1:35
for H being ZF-formula st H is conditional holds
( H is negative &amp; the_argument_of H is conjunctive &amp; the_right_argument_of (the_argument_of H) is negative )
proofend;

theorem :: ZF_LANG1:36
for H being ZF-formula st H is biconditional holds
( H is conjunctive &amp; the_left_argument_of H is conditional &amp; the_right_argument_of H is conditional )
proofend;

theorem :: ZF_LANG1:37
for H being ZF-formula st H is existential holds
( H is negative &amp; the_argument_of H is universal &amp; the_scope_of (the_argument_of H) is negative )
proofend;

theorem :: ZF_LANG1:38
for H being ZF-formula holds
( ( not H is being_equality or ( not H is being_membership &amp; not H is negative &amp; not H is conjunctive &amp; not H is universal ) ) &amp; ( not H is being_membership or ( not H is negative &amp; not H is conjunctive &amp; not H is universal ) ) &amp; ( not H is negative or ( not H is conjunctive &amp; not H is universal ) ) &amp; ( not H is conjunctive or not H is universal ) )
proofend;

theorem Th39: :: ZF_LANG1:39
for F, G being ZF-formula st F is_subformula_of G holds
len F <= len G
proofend;

theorem Th40: :: ZF_LANG1:40
for F, G, H being ZF-formula st ( ( F is_proper_subformula_of G &amp; G is_subformula_of H ) or ( F is_subformula_of G &amp; G is_proper_subformula_of H ) or ( F is_subformula_of G &amp; G is_immediate_constituent_of H ) or ( F is_immediate_constituent_of G &amp; G is_subformula_of H ) or ( F is_proper_subformula_of G &amp; G is_immediate_constituent_of H ) or ( F is_immediate_constituent_of G &amp; G is_proper_subformula_of H ) ) holds
F is_proper_subformula_of H
proofend;

theorem :: ZF_LANG1:41
for H being ZF-formula holds not H is_immediate_constituent_of H
proofend;

theorem :: ZF_LANG1:42
for G, H being ZF-formula holds
( not G is_proper_subformula_of H or not H is_subformula_of G )
proofend;

theorem :: ZF_LANG1:43
for G, H being ZF-formula holds
( not G is_proper_subformula_of H or not H is_proper_subformula_of G )
proofend;

theorem :: ZF_LANG1:44
for G, H being ZF-formula holds
( not G is_subformula_of H or not H is_immediate_constituent_of G )
proofend;

theorem :: ZF_LANG1:45
for G, H being ZF-formula holds
( not G is_proper_subformula_of H or not H is_immediate_constituent_of G )
proofend;

theorem :: ZF_LANG1:46
for F, H being ZF-formula st 'not' F is_subformula_of H holds
F is_proper_subformula_of H
proofend;

theorem :: ZF_LANG1:47
for F, G, H being ZF-formula st F '&amp;' G is_subformula_of H holds
( F is_proper_subformula_of H &amp; G is_proper_subformula_of H )
proofend;

theorem :: ZF_LANG1:48
for H, F being ZF-formula
for x being Variable st All (x,H) is_subformula_of F holds
H is_proper_subformula_of F
proofend;

theorem :: ZF_LANG1:49
for F, G being ZF-formula holds
( F '&amp;' ('not' G) is_proper_subformula_of F => G &amp; F is_proper_subformula_of F => G &amp; 'not' G is_proper_subformula_of F => G &amp; G is_proper_subformula_of F => G )
proofend;

theorem :: ZF_LANG1:50
for F, G being ZF-formula holds
( ('not' F) '&amp;' ('not' G) is_proper_subformula_of F 'or' G &amp; 'not' F is_proper_subformula_of F 'or' G &amp; 'not' G is_proper_subformula_of F 'or' G &amp; F is_proper_subformula_of F 'or' G &amp; G is_proper_subformula_of F 'or' G )
proofend;

theorem :: ZF_LANG1:51
for H being ZF-formula
for x being Variable holds
( All (x,('not' H)) is_proper_subformula_of Ex (x,H) &amp; 'not' H is_proper_subformula_of Ex (x,H) )
proofend;

theorem :: ZF_LANG1:52
for G, H being ZF-formula holds
( G is_subformula_of H iff G in Subformulae H ) by ZF_LANG:78, ZF_LANG:def_42;

theorem :: ZF_LANG1:53
for G, H being ZF-formula st G in Subformulae H holds
Subformulae G c= Subformulae H by ZF_LANG:78, ZF_LANG:79;

theorem :: ZF_LANG1:54
for H being ZF-formula holds H in Subformulae H
proofend;

theorem Th55: :: ZF_LANG1:55
for F, G being ZF-formula holds Subformulae (F => G) = ((Subformulae F) \/ (Subformulae G)) \/ {('not' G),(F '&amp;' ('not' G)),(F => G)}
proofend;

theorem :: ZF_LANG1:56
for F, G being ZF-formula holds Subformulae (F 'or' G) = ((Subformulae F) \/ (Subformulae G)) \/ {('not' G),('not' F),(('not' F) '&amp;' ('not' G)),(F 'or' G)}
proofend;

theorem :: ZF_LANG1:57
for F, G being ZF-formula holds Subformulae (F <=> G) = ((Subformulae F) \/ (Subformulae G)) \/ {('not' G),(F '&amp;' ('not' G)),(F => G),('not' F),(G '&amp;' ('not' F)),(G => F),(F <=> G)}
proofend;

theorem Th58: :: ZF_LANG1:58
for x, y being Variable holds Free (x '=' y) = {x,y}
proofend;

theorem Th59: :: ZF_LANG1:59
for x, y being Variable holds Free (x 'in' y) = {x,y}
proofend;

theorem Th60: :: ZF_LANG1:60
for p being ZF-formula holds Free ('not' p) = Free p
proofend;

theorem Th61: :: ZF_LANG1:61
for p, q being ZF-formula holds Free (p '&amp;' q) = (Free p) \/ (Free q)
proofend;

theorem Th62: :: ZF_LANG1:62
for p being ZF-formula
for x being Variable holds Free (All (x,p)) = (Free p) \ {x}
proofend;

theorem :: ZF_LANG1:63
for p, q being ZF-formula holds Free (p 'or' q) = (Free p) \/ (Free q)
proofend;

theorem Th64: :: ZF_LANG1:64
for p, q being ZF-formula holds Free (p => q) = (Free p) \/ (Free q)
proofend;

theorem :: ZF_LANG1:65
for p, q being ZF-formula holds Free (p <=> q) = (Free p) \/ (Free q)
proofend;

theorem Th66: :: ZF_LANG1:66
for p being ZF-formula
for x being Variable holds Free (Ex (x,p)) = (Free p) \ {x}
proofend;

theorem Th67: :: ZF_LANG1:67
for p being ZF-formula
for x, y being Variable holds Free (All (x,y,p)) = (Free p) \ {x,y}
proofend;

theorem :: ZF_LANG1:68
for p being ZF-formula
for x, y, z being Variable holds Free (All (x,y,z,p)) = (Free p) \ {x,y,z}
proofend;

theorem Th69: :: ZF_LANG1:69
for p being ZF-formula
for x, y being Variable holds Free (Ex (x,y,p)) = (Free p) \ {x,y}
proofend;

theorem :: ZF_LANG1:70
for p being ZF-formula
for x, y, z being Variable holds Free (Ex (x,y,z,p)) = (Free p) \ {x,y,z}
proofend;

scheme :: ZF_LANG1:sch 1
ZFInduction{ P1[ ZF-formula] } :
 for H being ZF-formula holds P1[H]
provided
A1: for x1, x2 being Variable holds
( P1[x1 '=' x2] &amp; P1[x1 'in' x2] ) and
A2: for H being ZF-formula st P1[H] holds
P1[ 'not' H] and
A3: for H1, H2 being ZF-formula st P1[H1] &amp; P1[H2] holds
P1[H1 '&amp;' H2] and
A4: for H being ZF-formula
for x being Variable st P1[H] holds
P1[ All (x,H)]
proofend;

definition
let D, D1, D2 be non empty set ;
let f be Function of D,D1;
assume A1: D1 c= D2 ;
funcD2 ! f ->  Function of D,D2 equals :: ZF_LANG1:def 1
f;
correctness
coherence
f is Function of D,D2;
proofend;
end;

:: deftheorem  defines ! ZF_LANG1:def_1_:_
 for D, D1, D2 being non empty set
for f being Function of D,D1 st D1 c= D2 holds
D2 ! f = f;

notation
let E be non empty set ;
let f be Function of VAR,E;
let x be Variable;
let e be Element of E;
synonym f / (x,e) for E +* (f,x);
end;

definition
let E be non empty set ;
let f be Function of VAR,E;
let x be Variable;
let e be Element of E;
:: original:/
redefine funcf / (x,e) ->  Function of VAR,E;
coherence
 x / (e,) is Function of VAR,E
proofend;
end;

theorem Th71: :: ZF_LANG1:71
for H being ZF-formula
for x being Variable
for M being non empty set
for v being Function of VAR,M holds
( M,v |= All (x,H) iff for m being Element of M holds M,v / (x,m) |= H )
proofend;

theorem Th72: :: ZF_LANG1:72
for H being ZF-formula
for x being Variable
for M being non empty set
for m being Element of M
for v being Function of VAR,M holds
( M,v |= All (x,H) iff M,v / (x,m) |= All (x,H) )
proofend;

theorem Th73: :: ZF_LANG1:73
for H being ZF-formula
for x being Variable
for M being non empty set
for v being Function of VAR,M holds
( M,v |= Ex (x,H) iff ex m being Element of M st M,v / (x,m) |= H )
proofend;

theorem :: ZF_LANG1:74
for H being ZF-formula
for x being Variable
for M being non empty set
for m being Element of M
for v being Function of VAR,M holds
( M,v |= Ex (x,H) iff M,v / (x,m) |= Ex (x,H) )
proofend;

theorem :: ZF_LANG1:75
for H being ZF-formula
for M being non empty set
for v, v9 being Function of VAR,M st ( for x being Variable st x in Free H holds
v9 . x = v . x ) &amp; M,v |= H holds
M,v9 |= H
proofend;

registration
let H be ZF-formula;
cluster Free H ->  finite ;
coherence
 Free H is finite
proofend;
end;

theorem :: ZF_LANG1:76
for i, j being Element of NAT st x. i = x. j holds
i = j ;

theorem :: ZF_LANG1:77
for x being Variable ex i being Element of NAT st x = x. i
proofend;

theorem Th78: :: ZF_LANG1:78
for x being Variable
for M being non empty set
for v being Function of VAR,M holds M,v |= x '=' x
proofend;

theorem Th79: :: ZF_LANG1:79
for x being Variable
for M being non empty set holds M |= x '=' x
proofend;

theorem Th80: :: ZF_LANG1:80
for x being Variable
for M being non empty set
for v being Function of VAR,M holds not M,v |= x 'in' x
proofend;

theorem Th81: :: ZF_LANG1:81
for x being Variable
for M being non empty set holds
( not M |= x 'in' x &amp; M |= 'not' (x 'in' x) )
proofend;

theorem :: ZF_LANG1:82
for x, y being Variable
for M being non empty set holds
( M |= x '=' y iff ( x = y or ex a being set st {a} = M ) )
proofend;

theorem :: ZF_LANG1:83
for x, y being Variable
for M being non empty set holds
( M |= 'not' (x 'in' y) iff ( x = y or for X being set st X in M holds
X misses M ) )
proofend;

theorem :: ZF_LANG1:84
for H being ZF-formula
for M being non empty set
for v being Function of VAR,M st H is being_equality holds
( M,v |= H iff v . (Var1 H) = v . (Var2 H) )
proofend;

theorem :: ZF_LANG1:85
for H being ZF-formula
for M being non empty set
for v being Function of VAR,M st H is being_membership holds
( M,v |= H iff v . (Var1 H) in v . (Var2 H) )
proofend;

theorem :: ZF_LANG1:86
for H being ZF-formula
for M being non empty set
for v being Function of VAR,M st H is negative holds
( M,v |= H iff not M,v |= the_argument_of H )
proofend;

theorem :: ZF_LANG1:87
for H being ZF-formula
for M being non empty set
for v being Function of VAR,M st H is conjunctive holds
( M,v |= H iff ( M,v |= the_left_argument_of H &amp; M,v |= the_right_argument_of H ) )
proofend;

theorem :: ZF_LANG1:88
for H being ZF-formula
for M being non empty set
for v being Function of VAR,M st H is universal holds
( M,v |= H iff for m being Element of M holds M,v / ((bound_in H),m) |= the_scope_of H )
proofend;

theorem :: ZF_LANG1:89
for H being ZF-formula
for M being non empty set
for v being Function of VAR,M st H is disjunctive holds
( M,v |= H iff ( M,v |= the_left_argument_of H or M,v |= the_right_argument_of H ) )
proofend;

theorem :: ZF_LANG1:90
for H being ZF-formula
for M being non empty set
for v being Function of VAR,M st H is conditional holds
( M,v |= H iff ( M,v |= the_antecedent_of H implies M,v |= the_consequent_of H ) )
proofend;

theorem :: ZF_LANG1:91
for H being ZF-formula
for M being non empty set
for v being Function of VAR,M st H is biconditional holds
( M,v |= H iff ( M,v |= the_left_side_of H iff M,v |= the_right_side_of H ) )
proofend;

theorem :: ZF_LANG1:92
for H being ZF-formula
for M being non empty set
for v being Function of VAR,M st H is existential holds
( M,v |= H iff ex m being Element of M st M,v / ((bound_in H),m) |= the_scope_of H )
proofend;

theorem :: ZF_LANG1:93
for H being ZF-formula
for x being Variable
for M being non empty set holds
( M |= Ex (x,H) iff for v being Function of VAR,M ex m being Element of M st M,v / (x,m) |= H )
proofend;

theorem Th94: :: ZF_LANG1:94
for H being ZF-formula
for x being Variable
for M being non empty set st M |= H holds
M |= Ex (x,H)
proofend;

theorem Th95: :: ZF_LANG1:95
for H being ZF-formula
for x, y being Variable
for M being non empty set holds
( M |= H iff M |= All (x,y,H) )
proofend;

theorem Th96: :: ZF_LANG1:96
for H being ZF-formula
for x, y being Variable
for M being non empty set st M |= H holds
M |= Ex (x,y,H)
proofend;

theorem :: ZF_LANG1:97
for H being ZF-formula
for x, y, z being Variable
for M being non empty set holds
( M |= H iff M |= All (x,y,z,H) )
proofend;

theorem :: ZF_LANG1:98
for H being ZF-formula
for x, y, z being Variable
for M being non empty set st M |= H holds
M |= Ex (x,y,z,H)
proofend;

::
:: Axioms of Logic
::
theorem :: ZF_LANG1:99
for p, q being ZF-formula
for M being non empty set
for v being Function of VAR,M holds
( M,v |= (p <=> q) => (p => q) &amp; M |= (p <=> q) => (p => q) )
proofend;

theorem :: ZF_LANG1:100
for p, q being ZF-formula
for M being non empty set
for v being Function of VAR,M holds
( M,v |= (p <=> q) => (q => p) &amp; M |= (p <=> q) => (q => p) )
proofend;

theorem Th101: :: ZF_LANG1:101
for p, q, r being ZF-formula
for M being non empty set holds M |= (p => q) => ((q => r) => (p => r))
proofend;

theorem Th102: :: ZF_LANG1:102
for p, q, r being ZF-formula
for M being non empty set
for v being Function of VAR,M st M,v |= p => q &amp; M,v |= q => r holds
M,v |= p => r
proofend;

theorem :: ZF_LANG1:103
for p, q, r being ZF-formula
for M being non empty set st M |= p => q &amp; M |= q => r holds
M |= p => r
proofend;

theorem :: ZF_LANG1:104
for p, q, r being ZF-formula
for M being non empty set
for v being Function of VAR,M holds
( M,v |= ((p => q) '&amp;' (q => r)) => (p => r) &amp; M |= ((p => q) '&amp;' (q => r)) => (p => r) )
proofend;

theorem :: ZF_LANG1:105
for p, q being ZF-formula
for M being non empty set
for v being Function of VAR,M holds
( M,v |= p => (q => p) &amp; M |= p => (q => p) )
proofend;

theorem :: ZF_LANG1:106
for p, q, r being ZF-formula
for M being non empty set
for v being Function of VAR,M holds
( M,v |= (p => (q => r)) => ((p => q) => (p => r)) &amp; M |= (p => (q => r)) => ((p => q) => (p => r)) )
proofend;

theorem :: ZF_LANG1:107
for p, q being ZF-formula
for M being non empty set
for v being Function of VAR,M holds
( M,v |= (p '&amp;' q) => p &amp; M |= (p '&amp;' q) => p )
proofend;

theorem :: ZF_LANG1:108
for p, q being ZF-formula
for M being non empty set
for v being Function of VAR,M holds
( M,v |= (p '&amp;' q) => q &amp; M |= (p '&amp;' q) => q )
proofend;

theorem :: ZF_LANG1:109
for p, q being ZF-formula
for M being non empty set
for v being Function of VAR,M holds
( M,v |= (p '&amp;' q) => (q '&amp;' p) &amp; M |= (p '&amp;' q) => (q '&amp;' p) )
proofend;

theorem :: ZF_LANG1:110
for p being ZF-formula
for M being non empty set
for v being Function of VAR,M holds
( M,v |= p => (p '&amp;' p) &amp; M |= p => (p '&amp;' p) )
proofend;

theorem :: ZF_LANG1:111
for p, q, r being ZF-formula
for M being non empty set
for v being Function of VAR,M holds
( M,v |= (p => q) => ((p => r) => (p => (q '&amp;' r))) &amp; M |= (p => q) => ((p => r) => (p => (q '&amp;' r))) )
proofend;

theorem Th112: :: ZF_LANG1:112
for p, q being ZF-formula
for M being non empty set
for v being Function of VAR,M holds
( M,v |= p => (p 'or' q) &amp; M |= p => (p 'or' q) )
proofend;

theorem :: ZF_LANG1:113
for q, p being ZF-formula
for M being non empty set
for v being Function of VAR,M holds
( M,v |= q => (p 'or' q) &amp; M |= q => (p 'or' q) )
proofend;

theorem :: ZF_LANG1:114
for p, q being ZF-formula
for M being non empty set
for v being Function of VAR,M holds
( M,v |= (p 'or' q) => (q 'or' p) &amp; M |= (p 'or' q) => (q 'or' p) )
proofend;

theorem :: ZF_LANG1:115
for p being ZF-formula
for M being non empty set
for v being Function of VAR,M holds
( M,v |= p => (p 'or' p) &amp; M |= p => (p 'or' p) ) by Th112;

theorem :: ZF_LANG1:116
for p, r, q being ZF-formula
for M being non empty set
for v being Function of VAR,M holds
( M,v |= (p => r) => ((q => r) => ((p 'or' q) => r)) &amp; M |= (p => r) => ((q => r) => ((p 'or' q) => r)) )
proofend;

theorem :: ZF_LANG1:117
for p, r, q being ZF-formula
for M being non empty set
for v being Function of VAR,M holds
( M,v |= ((p => r) '&amp;' (q => r)) => ((p 'or' q) => r) &amp; M |= ((p => r) '&amp;' (q => r)) => ((p 'or' q) => r) )
proofend;

theorem :: ZF_LANG1:118
for p, q being ZF-formula
for M being non empty set
for v being Function of VAR,M holds
( M,v |= (p => ('not' q)) => (q => ('not' p)) &amp; M |= (p => ('not' q)) => (q => ('not' p)) )
proofend;

theorem :: ZF_LANG1:119
for p, q being ZF-formula
for M being non empty set
for v being Function of VAR,M holds
( M,v |= ('not' p) => (p => q) &amp; M |= ('not' p) => (p => q) )
proofend;

theorem :: ZF_LANG1:120
for p, q being ZF-formula
for M being non empty set
for v being Function of VAR,M holds
( M,v |= ((p => q) '&amp;' (p => ('not' q))) => ('not' p) &amp; M |= ((p => q) '&amp;' (p => ('not' q))) => ('not' p) )
proofend;

theorem :: ZF_LANG1:121
for p, q being ZF-formula
for M being non empty set st M |= p => q &amp; M |= p holds
M |= q
proofend;

theorem :: ZF_LANG1:122
for p, q being ZF-formula
for M being non empty set
for v being Function of VAR,M holds
( M,v |= ('not' (p '&amp;' q)) => (('not' p) 'or' ('not' q)) &amp; M |= ('not' (p '&amp;' q)) => (('not' p) 'or' ('not' q)) )
proofend;

theorem :: ZF_LANG1:123
for p, q being ZF-formula
for M being non empty set
for v being Function of VAR,M holds
( M,v |= (('not' p) 'or' ('not' q)) => ('not' (p '&amp;' q)) &amp; M |= (('not' p) 'or' ('not' q)) => ('not' (p '&amp;' q)) )
proofend;

theorem :: ZF_LANG1:124
for p, q being ZF-formula
for M being non empty set
for v being Function of VAR,M holds
( M,v |= ('not' (p 'or' q)) => (('not' p) '&amp;' ('not' q)) &amp; M |= ('not' (p 'or' q)) => (('not' p) '&amp;' ('not' q)) )
proofend;

theorem :: ZF_LANG1:125
for p, q being ZF-formula
for M being non empty set
for v being Function of VAR,M holds
( M,v |= (('not' p) '&amp;' ('not' q)) => ('not' (p 'or' q)) &amp; M |= (('not' p) '&amp;' ('not' q)) => ('not' (p 'or' q)) )
proofend;

theorem :: ZF_LANG1:126
for H being ZF-formula
for x being Variable
for M being non empty set holds M |= (All (x,H)) => H
proofend;

theorem :: ZF_LANG1:127
for H being ZF-formula
for x being Variable
for M being non empty set holds M |= H => (Ex (x,H))
proofend;

theorem Th128: :: ZF_LANG1:128
for H1, H2 being ZF-formula
for x being Variable
for M being non empty set st not x in Free H1 holds
M |= (All (x,(H1 => H2))) => (H1 => (All (x,H2)))
proofend;

theorem :: ZF_LANG1:129
for H1, H2 being ZF-formula
for x being Variable
for M being non empty set st not x in Free H1 &amp; M |= H1 => H2 holds
M |= H1 => (All (x,H2))
proofend;

theorem Th130: :: ZF_LANG1:130
for H2, H1 being ZF-formula
for x being Variable
for M being non empty set st not x in Free H2 holds
M |= (All (x,(H1 => H2))) => ((Ex (x,H1)) => H2)
proofend;

theorem :: ZF_LANG1:131
for H2, H1 being ZF-formula
for x being Variable
for M being non empty set st not x in Free H2 &amp; M |= H1 => H2 holds
M |= (Ex (x,H1)) => H2
proofend;

theorem :: ZF_LANG1:132
for H1, H2 being ZF-formula
for x being Variable
for M being non empty set st M |= H1 => (All (x,H2)) holds
M |= H1 => H2
proofend;

theorem :: ZF_LANG1:133
for H1, H2 being ZF-formula
for x being Variable
for M being non empty set st M |= (Ex (x,H1)) => H2 holds
M |= H1 => H2
proofend;

theorem :: ZF_LANG1:134
WFF c= bool [:NAT,NAT:]
proofend;

::
:: Variables in ZF-formula
::
definition
let H be ZF-formula;
func variables_in H ->  set  equals :: ZF_LANG1:def 2
(rng H) \ {0,1,2,3,4};
correctness
coherence
(rng H) \ {0,1,2,3,4} is set ;
;
end;

:: deftheorem  defines variables_in ZF_LANG1:def_2_:_
 for H being ZF-formula holds variables_in H = (rng H) \ {0,1,2,3,4};

theorem Th135: :: ZF_LANG1:135
for x being Variable holds
( x <> 0 &amp; x <> 1 &amp; x <> 2 &amp; x <> 3 &amp; x <> 4 )
proofend;

theorem Th136: :: ZF_LANG1:136
for x being Variable holds not x in {0,1,2,3,4}
proofend;

theorem Th137: :: ZF_LANG1:137
for H being ZF-formula
for a being set st a in variables_in H holds
( a <> 0 &amp; a <> 1 &amp; a <> 2 &amp; a <> 3 &amp; a <> 4 )
proofend;

theorem Th138: :: ZF_LANG1:138
for x, y being Variable holds variables_in (x '=' y) = {x,y}
proofend;

theorem Th139: :: ZF_LANG1:139
for x, y being Variable holds variables_in (x 'in' y) = {x,y}
proofend;

theorem Th140: :: ZF_LANG1:140
for H being ZF-formula holds variables_in ('not' H) = variables_in H
proofend;

theorem Th141: :: ZF_LANG1:141
for H1, H2 being ZF-formula holds variables_in (H1 '&amp;' H2) = (variables_in H1) \/ (variables_in H2)
proofend;

theorem Th142: :: ZF_LANG1:142
for H being ZF-formula
for x being Variable holds variables_in (All (x,H)) = (variables_in H) \/ {x}
proofend;

theorem :: ZF_LANG1:143
for H1, H2 being ZF-formula holds variables_in (H1 'or' H2) = (variables_in H1) \/ (variables_in H2)
proofend;

theorem Th144: :: ZF_LANG1:144
for H1, H2 being ZF-formula holds variables_in (H1 => H2) = (variables_in H1) \/ (variables_in H2)
proofend;

theorem :: ZF_LANG1:145
for H1, H2 being ZF-formula holds variables_in (H1 <=> H2) = (variables_in H1) \/ (variables_in H2)
proofend;

theorem Th146: :: ZF_LANG1:146
for H being ZF-formula
for x being Variable holds variables_in (Ex (x,H)) = (variables_in H) \/ {x}
proofend;

theorem Th147: :: ZF_LANG1:147
for H being ZF-formula
for x, y being Variable holds variables_in (All (x,y,H)) = (variables_in H) \/ {x,y}
proofend;

theorem Th148: :: ZF_LANG1:148
for H being ZF-formula
for x, y being Variable holds variables_in (Ex (x,y,H)) = (variables_in H) \/ {x,y}
proofend;

theorem :: ZF_LANG1:149
for H being ZF-formula
for x, y, z being Variable holds variables_in (All (x,y,z,H)) = (variables_in H) \/ {x,y,z}
proofend;

theorem :: ZF_LANG1:150
for H being ZF-formula
for x, y, z being Variable holds variables_in (Ex (x,y,z,H)) = (variables_in H) \/ {x,y,z}
proofend;

theorem :: ZF_LANG1:151
for H being ZF-formula holds Free H c= variables_in H
proofend;

definition
let H be ZF-formula;
:: original:variables_in
redefine func variables_in H ->  non empty Subset of VAR;
coherence
 variables_in H is non empty Subset of VAR
proofend;
end;

definition
let H be ZF-formula;
let x, y be Variable;
funcH / (x,y) ->  Function means :Def3: :: ZF_LANG1:def 3
( dom it = dom H &amp; ( for a being set st a in dom H holds
( ( H . a = x implies it . a = y ) &amp; ( H . a <> x implies it . a = H . a ) ) ) );
existence
 ex b1 being Function st
( dom b1 = dom H &amp; ( for a being set st a in dom H holds
( ( H . a = x implies b1 . a = y ) &amp; ( H . a <> x implies b1 . a = H . a ) ) ) )
proofend;
uniqueness
 for b1, b2 being Function st dom b1 = dom H &amp; ( for a being set st a in dom H holds
( ( H . a = x implies b1 . a = y ) &amp; ( H . a <> x implies b1 . a = H . a ) ) ) &amp; dom b2 = dom H &amp; ( for a being set st a in dom H holds
( ( H . a = x implies b2 . a = y ) &amp; ( H . a <> x implies b2 . a = H . a ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def3 defines / ZF_LANG1:def_3_:_
 for H being ZF-formula
for x, y being Variable
for b4 being Function holds
( b4 = H / (x,y) iff ( dom b4 = dom H &amp; ( for a being set st a in dom H holds
( ( H . a = x implies b4 . a = y ) &amp; ( H . a <> x implies b4 . a = H . a ) ) ) ) );

theorem Th152: :: ZF_LANG1:152
for x1, x2, y1, y2, z1, z2 being Variable holds
( (x1 '=' x2) / (y1,y2) = z1 '=' z2 iff ( ( x1 <> y1 &amp; x2 <> y1 &amp; z1 = x1 &amp; z2 = x2 ) or ( x1 = y1 &amp; x2 <> y1 &amp; z1 = y2 &amp; z2 = x2 ) or ( x1 <> y1 &amp; x2 = y1 &amp; z1 = x1 &amp; z2 = y2 ) or ( x1 = y1 &amp; x2 = y1 &amp; z1 = y2 &amp; z2 = y2 ) ) )
proofend;

theorem Th153: :: ZF_LANG1:153
for x1, x2, y1, y2 being Variable ex z1, z2 being Variable st (x1 '=' x2) / (y1,y2) = z1 '=' z2
proofend;

theorem Th154: :: ZF_LANG1:154
for x1, x2, y1, y2, z1, z2 being Variable holds
( (x1 'in' x2) / (y1,y2) = z1 'in' z2 iff ( ( x1 <> y1 &amp; x2 <> y1 &amp; z1 = x1 &amp; z2 = x2 ) or ( x1 = y1 &amp; x2 <> y1 &amp; z1 = y2 &amp; z2 = x2 ) or ( x1 <> y1 &amp; x2 = y1 &amp; z1 = x1 &amp; z2 = y2 ) or ( x1 = y1 &amp; x2 = y1 &amp; z1 = y2 &amp; z2 = y2 ) ) )
proofend;

theorem Th155: :: ZF_LANG1:155
for x1, x2, y1, y2 being Variable ex z1, z2 being Variable st (x1 'in' x2) / (y1,y2) = z1 'in' z2
proofend;

theorem Th156: :: ZF_LANG1:156
for F, H being ZF-formula
for x, y being Variable holds
( 'not' F = ('not' H) / (x,y) iff F = H / (x,y) )
proofend;

Lm1:  for G1, H1, G2, H2 being ZF-formula
for x, y being Variable st G1 = H1 / (x,y) &amp; G2 = H2 / (x,y) holds
G1 '&amp;' G2 = (H1 '&amp;' H2) / (x,y)
proofend;

Lm2:  for F, H being ZF-formula
for x, y, z, s being Variable st F = H / (x,y) &amp; ( ( z = s &amp; s <> x ) or ( z = y &amp; s = x ) ) holds
All (z,F) = (All (s,H)) / (x,y)
proofend;

theorem Th157: :: ZF_LANG1:157
for H being ZF-formula
for x, y being Variable holds H / (x,y) in WFF
proofend;

definition
let H be ZF-formula;
let x, y be Variable;
:: original:/
redefine funcH / (x,y) ->  ZF-formula;
coherence
 H / (x,y) is ZF-formula
proofend;
end;

theorem Th158: :: ZF_LANG1:158
for G1, G2, H1, H2 being ZF-formula
for x, y being Variable holds
( G1 '&amp;' G2 = (H1 '&amp;' H2) / (x,y) iff ( G1 = H1 / (x,y) &amp; G2 = H2 / (x,y) ) )
proofend;

theorem Th159: :: ZF_LANG1:159
for G, H being ZF-formula
for z, x, y being Variable st z <> x holds
( All (z,G) = (All (z,H)) / (x,y) iff G = H / (x,y) )
proofend;

theorem Th160: :: ZF_LANG1:160
for G, H being ZF-formula
for y, x being Variable holds
( All (y,G) = (All (x,H)) / (x,y) iff G = H / (x,y) )
proofend;

theorem Th161: :: ZF_LANG1:161
for G1, G2, H1, H2 being ZF-formula
for x, y being Variable holds
( G1 'or' G2 = (H1 'or' H2) / (x,y) iff ( G1 = H1 / (x,y) &amp; G2 = H2 / (x,y) ) )
proofend;

theorem Th162: :: ZF_LANG1:162
for G1, G2, H1, H2 being ZF-formula
for x, y being Variable holds
( G1 => G2 = (H1 => H2) / (x,y) iff ( G1 = H1 / (x,y) &amp; G2 = H2 / (x,y) ) )
proofend;

theorem Th163: :: ZF_LANG1:163
for G1, G2, H1, H2 being ZF-formula
for x, y being Variable holds
( G1 <=> G2 = (H1 <=> H2) / (x,y) iff ( G1 = H1 / (x,y) &amp; G2 = H2 / (x,y) ) )
proofend;

theorem Th164: :: ZF_LANG1:164
for G, H being ZF-formula
for z, x, y being Variable st z <> x holds
( Ex (z,G) = (Ex (z,H)) / (x,y) iff G = H / (x,y) )
proofend;

theorem Th165: :: ZF_LANG1:165
for G, H being ZF-formula
for y, x being Variable holds
( Ex (y,G) = (Ex (x,H)) / (x,y) iff G = H / (x,y) )
proofend;

theorem :: ZF_LANG1:166
for H being ZF-formula
for x, y being Variable holds
( H is being_equality iff H / (x,y) is being_equality )
proofend;

theorem :: ZF_LANG1:167
for H being ZF-formula
for x, y being Variable holds
( H is being_membership iff H / (x,y) is being_membership )
proofend;

theorem Th168: :: ZF_LANG1:168
for H being ZF-formula
for x, y being Variable holds
( H is negative iff H / (x,y) is negative )
proofend;

theorem Th169: :: ZF_LANG1:169
for H being ZF-formula
for x, y being Variable holds
( H is conjunctive iff H / (x,y) is conjunctive )
proofend;

theorem Th170: :: ZF_LANG1:170
for H being ZF-formula
for x, y being Variable holds
( H is universal iff H / (x,y) is universal )
proofend;

theorem :: ZF_LANG1:171
for H being ZF-formula
for x, y being Variable st H is negative holds
the_argument_of (H / (x,y)) = (the_argument_of H) / (x,y)
proofend;

theorem :: ZF_LANG1:172
for H being ZF-formula
for x, y being Variable st H is conjunctive holds
( the_left_argument_of (H / (x,y)) = (the_left_argument_of H) / (x,y) &amp; the_right_argument_of (H / (x,y)) = (the_right_argument_of H) / (x,y) )
proofend;

theorem :: ZF_LANG1:173
for H being ZF-formula
for x, y being Variable st H is universal holds
( the_scope_of (H / (x,y)) = (the_scope_of H) / (x,y) &amp; ( bound_in H = x implies bound_in (H / (x,y)) = y ) &amp; ( bound_in H <> x implies bound_in (H / (x,y)) = bound_in H ) )
proofend;

theorem Th174: :: ZF_LANG1:174
for H being ZF-formula
for x, y being Variable holds
( H is disjunctive iff H / (x,y) is disjunctive )
proofend;

theorem Th175: :: ZF_LANG1:175
for H being ZF-formula
for x, y being Variable holds
( H is conditional iff H / (x,y) is conditional )
proofend;

theorem Th176: :: ZF_LANG1:176
for H being ZF-formula
for x, y being Variable st H is biconditional holds
H / (x,y) is biconditional
proofend;

theorem Th177: :: ZF_LANG1:177
for H being ZF-formula
for x, y being Variable holds
( H is existential iff H / (x,y) is existential )
proofend;

theorem :: ZF_LANG1:178
for H being ZF-formula
for x, y being Variable st H is disjunctive holds
( the_left_argument_of (H / (x,y)) = (the_left_argument_of H) / (x,y) &amp; the_right_argument_of (H / (x,y)) = (the_right_argument_of H) / (x,y) )
proofend;

theorem :: ZF_LANG1:179
for H being ZF-formula
for x, y being Variable st H is conditional holds
( the_antecedent_of (H / (x,y)) = (the_antecedent_of H) / (x,y) &amp; the_consequent_of (H / (x,y)) = (the_consequent_of H) / (x,y) )
proofend;

theorem :: ZF_LANG1:180
for H being ZF-formula
for x, y being Variable st H is biconditional holds
( the_left_side_of (H / (x,y)) = (the_left_side_of H) / (x,y) &amp; the_right_side_of (H / (x,y)) = (the_right_side_of H) / (x,y) )
proofend;

theorem :: ZF_LANG1:181
for H being ZF-formula
for x, y being Variable st H is existential holds
( the_scope_of (H / (x,y)) = (the_scope_of H) / (x,y) &amp; ( bound_in H = x implies bound_in (H / (x,y)) = y ) &amp; ( bound_in H <> x implies bound_in (H / (x,y)) = bound_in H ) )
proofend;

theorem Th182: :: ZF_LANG1:182
for H being ZF-formula
for x, y being Variable st not x in variables_in H holds
H / (x,y) = H
proofend;

theorem :: ZF_LANG1:183
for H being ZF-formula
for x being Variable holds H / (x,x) = H
proofend;

theorem Th184: :: ZF_LANG1:184
for H being ZF-formula
for x, y being Variable st x <> y holds
not x in variables_in (H / (x,y))
proofend;

theorem :: ZF_LANG1:185
for H being ZF-formula
for x, y being Variable st x in variables_in H holds
y in variables_in (H / (x,y))
proofend;

theorem :: ZF_LANG1:186
for H being ZF-formula
for x, y, z being Variable st x <> y holds
(H / (x,y)) / (x,z) = H / (x,y)
proofend;

theorem :: ZF_LANG1:187
for H being ZF-formula
for x, y being Variable holds variables_in (H / (x,y)) c= ((variables_in H) \ {x}) \/ {y}
proofend;