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


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

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

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

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 )
proof end;

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 )
proof end;

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

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

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

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

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 & bound_in (All (x,y,p)) = x & the_scope_of (All (x,y,p)) = All (y,p) ) by Th8;

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

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))))) & All (x,y,z,p) = All (x,y,(All (z,p))) ) ;

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

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

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

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

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))))) & Ex (x,y,z,p) = Ex (x,y,(Ex (z,p))) ) ;

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

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

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

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

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))
proof end;

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))
proof end;

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)
proof end;

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))
proof end;

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) & the_left_side_of H = the_consequent_of (the_right_argument_of H) )
proof end;

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) & the_right_side_of H = the_antecedent_of (the_right_argument_of H) )
proof end;

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

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

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

theorem :: ZF_LANG1:32
for F, G being ZF-formula holds
( the_left_argument_of (F <=> G) = F => G & 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 & H is negative & the_argument_of H is conjunctive & the_left_argument_of (the_argument_of H) is negative & the_right_argument_of (the_argument_of H) is negative )
proof end;

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

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

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

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

theorem Th39: :: ZF_LANG1:39
for F, G being ZF-formula st F is_subformula_of G holds
len F <= len G by ZF_LANG:def 41, ZF_LANG:62;

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

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

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 )
proof end;

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 )
proof end;

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 )
proof end;

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 )
proof end;

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

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

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

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

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

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) & 'not' H is_proper_subformula_of Ex (x,H) )
proof end;

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
proof end;

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

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) '&' ('not' G)),(F 'or' G)}
proof end;

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

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

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

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

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

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

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

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

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

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

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}
proof end;

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}
proof end;

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}
proof end;

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}
proof end;

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] & 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] & P1[H2] holds
P1[H1 '&' H2] and
A4: for H being ZF-formula
for x being Variable st P1[H] holds
P1[ All (x,H)]
proof end;

definition
let D, D1, D2 be non empty set ;
let f be Function of D,D1;
assume A1: D1 c= D2 ;
func D2 ! f -> Function of D,D2 equals :: ZF_LANG1:def 1
f;
correctness
coherence
f is Function of D,D2;
proof end;
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 func f / (x,e) -> Function of VAR,E;
coherence
x / (e,) is Function of VAR,E
proof end;
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 )
proof end;

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) )
proof end;

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 )
proof end;

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) )
proof end;

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 ) & M,v |= H holds
M,v9 |= H
proof end;

registration
let H be ZF-formula;
cluster Free H -> finite ;
coherence
Free H is finite
proof end;
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
proof end;

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
proof end;

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

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
proof end;

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

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 ) )
proof end;

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 ) )
proof end;

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) )
proof end;

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) )
proof end;

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 )
proof end;

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 & M,v |= the_right_argument_of H ) )
proof end;

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 )
proof end;

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 ) )
proof end;

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 ) )
proof end;

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 ) )
proof end;

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 )
proof end;

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 )
proof end;

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)
proof end;

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) )
proof end;

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)
proof end;

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) )
proof end;

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)
proof end;

::
:: 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) & M |= (p <=> q) => (p => q) )
proof end;

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) & M |= (p <=> q) => (q => p) )
proof end;

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))
proof end;

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 & M,v |= q => r holds
M,v |= p => r
proof end;

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

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) '&' (q => r)) => (p => r) & M |= ((p => q) '&' (q => r)) => (p => r) )
proof end;

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) & M |= p => (q => p) )
proof end;

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)) & M |= (p => (q => r)) => ((p => q) => (p => r)) )
proof end;

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 '&' q) => p & M |= (p '&' q) => p )
proof end;

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 '&' q) => q & M |= (p '&' q) => q )
proof end;

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 '&' q) => (q '&' p) & M |= (p '&' q) => (q '&' p) )
proof end;

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 '&' p) & M |= p => (p '&' p) )
proof end;

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 '&' r))) & M |= (p => q) => ((p => r) => (p => (q '&' r))) )
proof end;

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) & M |= p => (p 'or' q) )
proof end;

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

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) & M |= (p 'or' q) => (q 'or' p) )
proof end;

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) & M |= p => (p 'or' p) ) by Th112;

theorem :: ZF_LANG1:116
for p, q, r 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)) & M |= (p => r) => ((q => r) => ((p 'or' q) => r)) )
proof end;

theorem :: ZF_LANG1:117
for p, q, r 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) & M |= ((p => r) '&' (q => r)) => ((p 'or' q) => r) )
proof end;

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)) & M |= (p => ('not' q)) => (q => ('not' p)) )
proof end;

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) & M |= ('not' p) => (p => q) )
proof end;

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) '&' (p => ('not' q))) => ('not' p) & M |= ((p => q) '&' (p => ('not' q))) => ('not' p) )
proof end;

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

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 '&' q)) => (('not' p) 'or' ('not' q)) & M |= ('not' (p '&' q)) => (('not' p) 'or' ('not' q)) )
proof end;

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 '&' q)) & M |= (('not' p) 'or' ('not' q)) => ('not' (p '&' q)) )
proof end;

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) '&' ('not' q)) & M |= ('not' (p 'or' q)) => (('not' p) '&' ('not' q)) )
proof end;

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) '&' ('not' q)) => ('not' (p 'or' q)) & M |= (('not' p) '&' ('not' q)) => ('not' (p 'or' q)) )
proof end;

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
proof end;

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))
proof end;

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)))
proof end;

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 & M |= H1 => H2 holds
M |= H1 => (All (x,H2))
proof end;

theorem Th130: :: ZF_LANG1:130
for H1, H2 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)
proof end;

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

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
proof end;

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
proof end;

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

::
:: 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 & x <> 1 & x <> 2 & x <> 3 & x <> 4 )
proof end;

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

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

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

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

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

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

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

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

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

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

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

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}
proof end;

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}
proof end;

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}
proof end;

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}
proof end;

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

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
proof end;
end;

definition
let H be ZF-formula;
let x, y be Variable;
func H / (x,y) -> Function means :Def3: :: ZF_LANG1:def 3
( dom it = dom H & ( for a being object st a in dom H holds
( ( H . a = x implies it . a = y ) & ( H . a <> x implies it . a = H . a ) ) ) );
existence
ex b1 being Function st
( dom b1 = dom H & ( for a being object st a in dom H holds
( ( H . a = x implies b1 . a = y ) & ( H . a <> x implies b1 . a = H . a ) ) ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = dom H & ( for a being object st a in dom H holds
( ( H . a = x implies b1 . a = y ) & ( H . a <> x implies b1 . a = H . a ) ) ) & dom b2 = dom H & ( for a being object st a in dom H holds
( ( H . a = x implies b2 . a = y ) & ( H . a <> x implies b2 . a = H . a ) ) ) holds
b1 = b2
proof end;
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 & ( for a being object st a in dom H holds
( ( H . a = x implies b4 . a = y ) & ( 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 & x2 <> y1 & z1 = x1 & z2 = x2 ) or ( x1 = y1 & x2 <> y1 & z1 = y2 & z2 = x2 ) or ( x1 <> y1 & x2 = y1 & z1 = x1 & z2 = y2 ) or ( x1 = y1 & x2 = y1 & z1 = y2 & z2 = y2 ) ) )
proof end;

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

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 & x2 <> y1 & z1 = x1 & z2 = x2 ) or ( x1 = y1 & x2 <> y1 & z1 = y2 & z2 = x2 ) or ( x1 <> y1 & x2 = y1 & z1 = x1 & z2 = y2 ) or ( x1 = y1 & x2 = y1 & z1 = y2 & z2 = y2 ) ) )
proof end;

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
proof end;

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) )
proof end;

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

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

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

definition
let H be ZF-formula;
let x, y be Variable;
:: original: /
redefine func H / (x,y) -> ZF-formula;
coherence
H / (x,y) is ZF-formula by Th157, ZF_LANG:4;
end;

theorem Th158: :: ZF_LANG1:158
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) & G2 = H2 / (x,y) ) )
proof end;

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

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

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) & G2 = H2 / (x,y) ) )
proof end;

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) & G2 = H2 / (x,y) ) )
proof end;

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) & G2 = H2 / (x,y) ) )
proof end;

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

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

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 )
proof end;

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 )
proof end;

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 )
proof end;

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 )
proof end;

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 )
proof end;

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)
proof end;

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) & the_right_argument_of (H / (x,y)) = (the_right_argument_of H) / (x,y) )
proof end;

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) & ( bound_in H = x implies bound_in (H / (x,y)) = y ) & ( bound_in H <> x implies bound_in (H / (x,y)) = bound_in H ) )
proof end;

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 )
proof end;

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 )
proof end;

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
proof end;

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 )
proof end;

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) & the_right_argument_of (H / (x,y)) = (the_right_argument_of H) / (x,y) )
proof end;

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) & the_consequent_of (H / (x,y)) = (the_consequent_of H) / (x,y) )
proof end;

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) & the_right_side_of (H / (x,y)) = (the_right_side_of H) / (x,y) )
proof end;

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) & ( bound_in H = x implies bound_in (H / (x,y)) = y ) & ( bound_in H <> x implies bound_in (H / (x,y)) = bound_in H ) )
proof end;

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
proof end;

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

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))
proof end;

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))
proof end;

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)
proof end;

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}
proof end;