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

begin

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

canceled;

theorem :: ZF_LANG1:12

canceled;

theorem :: ZF_LANG1:13

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, ZF_LANG:16;

theorem :: ZF_LANG1:14

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, ZF_LANG:22;

theorem :: ZF_LANG1:15

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 Th16: :: ZF_LANG1:16

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 & y1 = y2 & p1 = p2 )

proof end;

theorem :: ZF_LANG1:17

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 & y1 = y2 & z1 = z2 & p1 = p2 )

proof end;

theorem :: ZF_LANG1:18

canceled;

theorem :: ZF_LANG1:19

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

proof end;

theorem Th20: :: ZF_LANG1:20

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 & y1 = y2 & p1 = p2 )

proof end;

theorem :: ZF_LANG1:21

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

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 & y1 = y2 & z1 = z2 & p1 = p2 )

proof end;

theorem :: ZF_LANG1:23

canceled;

theorem :: ZF_LANG1:24

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

proof end;

theorem :: ZF_LANG1:25

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, ZF_LANG:16;

theorem :: ZF_LANG1:26

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, ZF_LANG:22;

theorem :: ZF_LANG1:27

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

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

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

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

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

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

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

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

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

theorem :: ZF_LANG1:36

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

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

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

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

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 )

proof end;

theorem :: ZF_LANG1:41

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

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 Th43: :: ZF_LANG1:43

for F, G being ZF-formula st F is_subformula_of G holds
len F <= len G

proof end;

theorem Th44: :: ZF_LANG1:44

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

canceled;

theorem :: ZF_LANG1:46

for H being ZF-formula holds not H is_immediate_constituent_of H

proof end;

theorem :: ZF_LANG1:47

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

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

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

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

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

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

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

proof end;

theorem :: ZF_LANG1:54

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

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

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

for G, H being ZF-formula holds
( G is_subformula_of H iff G in Subformulae H ) by ZF_LANG:100, ZF_LANG:def 42;

theorem :: ZF_LANG1:58

for G, H being ZF-formula st G in Subformulae H holds
Subformulae G c= Subformulae H by ZF_LANG:100, ZF_LANG:101;

theorem :: ZF_LANG1:59

for H being ZF-formula holds H in Subformulae H

proof end;

theorem Th60: :: ZF_LANG1:60

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

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

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 Th63: :: ZF_LANG1:63

for x, y being Variable holds Free (x '=' y) = {x,y}

proof end;

theorem Th64: :: ZF_LANG1:64

for x, y being Variable holds Free (x 'in' y) = {x,y}

proof end;

theorem Th65: :: ZF_LANG1:65

for p being ZF-formula holds Free ('not' p) = Free p

proof end;

theorem Th66: :: ZF_LANG1:66

for p, q being ZF-formula holds Free (p '&' q) = (Free p) \/ (Free q)

proof end;

theorem Th67: :: ZF_LANG1:67

for p being ZF-formula
for x being Variable holds Free (All (x,p)) = (Free p) \ {x}

proof end;

theorem :: ZF_LANG1:68

for p, q being ZF-formula holds Free (p 'or' q) = (Free p) \/ (Free q)

proof end;

theorem Th69: :: ZF_LANG1:69

for p, q being ZF-formula holds Free (p => q) = (Free p) \/ (Free q)

proof end;

theorem :: ZF_LANG1:70

for p, q being ZF-formula holds Free (p <=> q) = (Free p) \/ (Free q)

proof end;

theorem Th71: :: ZF_LANG1:71

for p being ZF-formula
for x being Variable holds Free (Ex (x,p)) = (Free p) \ {x}

proof end;

theorem Th72: :: ZF_LANG1:72

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

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 Th74: :: ZF_LANG1:74

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

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{ P₁[ ZF-formula] } :

for H being ZF-formula holds P₁[H]

provided

A1: for x1, x2 being Variable holds
( P₁[x1 '=' x2] & P₁[x1 'in' x2] ) and
A2: for H being ZF-formula st P₁[H] holds
P₁[ 'not' H] and
A3: for H1, H2 being ZF-formula st P₁[H1] & P₁[H2] holds
P₁[H1 '&' H2] and
A4: for H being ZF-formula
for x being Variable st P₁[H] holds
P₁[ All (x,H)]

proof end;

definition

let D, D1, D2 be non empty set ;
let f be Function of D,D1;
canceled;
assume A1: D1 c= D2 ;
func D2 ! f -> Function of D,D2 equals :: ZF_LANG1:def 2
f;
correctness
coherence
f is Function of D,D2;

proof end;

end;

:: deftheorem ZF_LANG1:def 1 :
canceled;

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

theorem :: ZF_LANG1:76

canceled;

theorem :: ZF_LANG1:77

canceled;

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 :: ZF_LANG1:78

canceled;

theorem :: ZF_LANG1:79

canceled;

theorem Th80: :: ZF_LANG1:80

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 Th81: :: ZF_LANG1:81

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 Th82: :: ZF_LANG1:82

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

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

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;

theorem :: ZF_LANG1:85

canceled;

registration

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

proof end;

end;

theorem :: ZF_LANG1:86

for i, j being Element of NAT st x. i = x. j holds
i = j ;

theorem :: ZF_LANG1:87

for x being Variable ex i being Element of NAT st x = x. i

proof end;

theorem :: ZF_LANG1:88

canceled;

theorem Th89: :: ZF_LANG1:89

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 Th90: :: ZF_LANG1:90

for x being Variable
for M being non empty set holds M |= x '=' x

proof end;

theorem Th91: :: ZF_LANG1:91

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 Th92: :: ZF_LANG1:92

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

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

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

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

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

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

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

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

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

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

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

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

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 Th105: :: ZF_LANG1:105

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 Th106: :: ZF_LANG1:106

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 Th107: :: ZF_LANG1:107

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

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

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;

theorem :: ZF_LANG1:110

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

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 Th112: :: ZF_LANG1:112

for p, q, r being ZF-formula
for M being non empty set holds M |= (p => q) => ((q => r) => (p => r))

proof end;

theorem Th113: :: ZF_LANG1:113

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

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

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

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

proof end;

theorem :: ZF_LANG1:121

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

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 Th123: :: 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 |= p => (p 'or' q) & M |= p => (p 'or' q) )

proof end;

theorem :: ZF_LANG1:124

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

proof end;

theorem :: ZF_LANG1:126

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 Th123;

theorem :: ZF_LANG1:127

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

proof end;

theorem :: ZF_LANG1:128

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

proof end;

theorem :: ZF_LANG1:129

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

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

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

canceled;

theorem :: ZF_LANG1:133

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

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

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

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

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

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

for H being ZF-formula
for x being Variable
for M being non empty set holds M |= H => (Ex (x,H))

proof end;

theorem Th140: :: ZF_LANG1:140

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

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 Th142: :: ZF_LANG1:142

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)

proof end;

theorem :: ZF_LANG1:143

for H2, H1 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:144

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

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

WFF c= bool [:NAT,NAT:]

proof end;

definition

let H be ZF-formula;
func variables_in H -> set equals :: ZF_LANG1:def 3
(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 3 :
for H being ZF-formula holds variables_in H = (rng H) \ {0,1,2,3,4};

theorem :: ZF_LANG1:147

canceled;

theorem Th148: :: ZF_LANG1:148

for x being Variable holds
( x <> 0 & x <> 1 & x <> 2 & x <> 3 & x <> 4 )

proof end;

theorem Th149: :: ZF_LANG1:149

for x being Variable holds not x in {0,1,2,3,4}

proof end;

theorem Th150: :: ZF_LANG1:150

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 Th151: :: ZF_LANG1:151

for x, y being Variable holds variables_in (x '=' y) = {x,y}

proof end;

theorem Th152: :: ZF_LANG1:152

for x, y being Variable holds variables_in (x 'in' y) = {x,y}

proof end;

theorem Th153: :: ZF_LANG1:153

for H being ZF-formula holds variables_in ('not' H) = variables_in H

proof end;

theorem Th154: :: ZF_LANG1:154

for H1, H2 being ZF-formula holds variables_in (H1 '&' H2) = (variables_in H1) \/ (variables_in H2)

proof end;

theorem Th155: :: ZF_LANG1:155

for H being ZF-formula
for x being Variable holds variables_in (All (x,H)) = (variables_in H) \/ {x}

proof end;

theorem :: ZF_LANG1:156

for H1, H2 being ZF-formula holds variables_in (H1 'or' H2) = (variables_in H1) \/ (variables_in H2)

proof end;

theorem Th157: :: ZF_LANG1:157

for H1, H2 being ZF-formula holds variables_in (H1 => H2) = (variables_in H1) \/ (variables_in H2)

proof end;

theorem :: ZF_LANG1:158

for H1, H2 being ZF-formula holds variables_in (H1 <=> H2) = (variables_in H1) \/ (variables_in H2)

proof end;

theorem Th159: :: ZF_LANG1:159

for H being ZF-formula
for x being Variable holds variables_in (Ex (x,H)) = (variables_in H) \/ {x}

proof end;

theorem Th160: :: ZF_LANG1:160

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 Th161: :: ZF_LANG1:161

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

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

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

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 :Def4: :: ZF_LANG1:def 4
( dom it = dom H & ( for a being set st a in dom H holds
( ( H . a = x implies it . a = y ) & ( H . a <> x implies it . a = H . a ) ) ) );
existence
ex b₁ being Function st
( dom b₁ = dom H & ( for a being set st a in dom H holds
( ( H . a = x implies b₁ . a = y ) & ( H . a <> x implies b₁ . a = H . a ) ) ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = dom H & ( for a being set st a in dom H holds
( ( H . a = x implies b₁ . a = y ) & ( H . a <> x implies b₁ . a = H . a ) ) ) & dom b₂ = dom H & ( for a being set st a in dom H holds
( ( H . a = x implies b₂ . a = y ) & ( H . a <> x implies b₂ . a = H . a ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines / ZF_LANG1:def 4 :
for H being ZF-formula
for x, y being Variable
for b₄ being Function holds
( b₄ = H / (x,y) iff ( dom b₄ = dom H & ( for a being set st a in dom H holds
( ( H . a = x implies b₄ . a = y ) & ( H . a <> x implies b₄ . a = H . a ) ) ) ) );

theorem :: ZF_LANG1:165

canceled;

theorem Th166: :: ZF_LANG1:166

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 Th167: :: ZF_LANG1:167

for x1, x2, y1, y2 being Variable ex z1, z2 being Variable st (x1 '=' x2) / (y1,y2) = z1 '=' z2

proof end;

theorem Th168: :: ZF_LANG1:168

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 Th169: :: ZF_LANG1:169

for x1, x2, y1, y2 being Variable ex z1, z2 being Variable st (x1 'in' x2) / (y1,y2) = z1 'in' z2

proof end;

theorem Th170: :: ZF_LANG1:170

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, H1, G2, 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 Th171: :: ZF_LANG1:171

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

proof end;

end;

theorem Th172: :: ZF_LANG1:172

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 Th173: :: ZF_LANG1:173

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

proof end;

theorem Th174: :: ZF_LANG1:174

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

proof end;

theorem Th175: :: ZF_LANG1:175

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 Th176: :: ZF_LANG1:176

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 Th177: :: ZF_LANG1:177

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 Th178: :: ZF_LANG1:178

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

proof end;

theorem Th179: :: ZF_LANG1:179

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

proof end;

theorem :: ZF_LANG1:180

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

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 Th182: :: ZF_LANG1:182

for H being ZF-formula
for x, y being Variable holds
( H is negative iff H / (x,y) is negative )

proof end;

theorem Th183: :: ZF_LANG1:183

for H being ZF-formula
for x, y being Variable holds
( H is conjunctive iff H / (x,y) is conjunctive )

proof end;

theorem Th184: :: ZF_LANG1:184

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

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

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

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 Th188: :: ZF_LANG1:188

for H being ZF-formula
for x, y being Variable holds
( H is disjunctive iff H / (x,y) is disjunctive )

proof end;

theorem Th189: :: ZF_LANG1:189

for H being ZF-formula
for x, y being Variable holds
( H is conditional iff H / (x,y) is conditional )

proof end;

theorem Th190: :: ZF_LANG1:190

for H being ZF-formula
for x, y being Variable st H is biconditional holds
H / (x,y) is biconditional

proof end;

theorem Th191: :: ZF_LANG1:191

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

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

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

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

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 Th196: :: ZF_LANG1:196

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

for H being ZF-formula
for x being Variable holds H / (x,x) = H

proof end;

theorem Th198: :: ZF_LANG1:198

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

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

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

for H being ZF-formula
for x, y being Variable holds variables_in (H / (x,y)) c= ((variables_in H) \ {x}) \/ {y}

proof end;