:: by Grzegorz Bancerek

::

:: Received August 10, 1990

:: Copyright (c) 1990-2012 Association of Mizar Users

begin

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 )

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

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

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

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 )

for x being Variable holds

( bound_in (Ex (x,p)) = x & the_scope_of (Ex (x,p)) = p )

proof end;

theorem :: ZF_LANG1:11

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

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

theorem :: ZF_LANG1:13

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

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

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

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

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

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

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

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

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

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

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

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)

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

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

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

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

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

( 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

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;

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

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 )

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

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

( H is conjunctive & the_left_argument_of H is conditional & the_right_argument_of H is conditional )

proof end;

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 )

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

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

F is_proper_subformula_of H

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 )

( not G is_proper_subformula_of H or not H is_proper_subformula_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 )

( not G is_proper_subformula_of H or not H is_immediate_constituent_of G )

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 )

( F is_proper_subformula_of H & G is_proper_subformula_of H )

proof end;

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

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 )

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

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

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;

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

Subformulae G c= Subformulae H by ZF_LANG:78, ZF_LANG:79;

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;

scheme :: ZF_LANG1:sch 1

ZFInduction{ P_{1}[ ZF-formula] } :

provided

ZFInduction{ P

provided

A1:
for x1, x2 being Variable holds

( P_{1}[x1 '=' x2] & P_{1}[x1 'in' x2] )
and

A2: for H being ZF-formula st P_{1}[H] holds

P_{1}[ 'not' H]
and

A3: for H1, H2 being ZF-formula st P_{1}[H1] & P_{1}[H2] holds

P_{1}[H1 '&' H2]
and

A4: for H being ZF-formula

for x being Variable st P_{1}[H] holds

P_{1}[ All (x,H)]

( P

A2: for H being ZF-formula st P

P

A3: for H1, H2 being ZF-formula st P

P

A4: for H being ZF-formula

for x being Variable st P

P

proof end;

definition

let D, D1, D2 be non empty set ;

let f be Function of D,D1;

assume A1: D1 c= D2 ;

correctness

coherence

f is Function of D,D2;

end;
let f be Function of D,D1;

assume A1: D1 c= D2 ;

correctness

coherence

f is Function of D,D2;

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

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

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

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

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 )

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

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 )

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

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

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

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

for M being non empty set

for v being Function of VAR,M holds not M,v |= 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 ) )

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

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

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

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 )

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

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 )

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

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

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

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 )

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 )

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

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)

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

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)

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

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

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

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

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

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

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

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

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 )

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 )

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

for x being Variable

for M being non empty set st M |= (Ex (x,H1)) => H2 holds

M |= H1 => H2

proof end;

::

:: Variables in ZF-formula

::

:: Variables in ZF-formula

::

:: deftheorem defines variables_in ZF_LANG1:def 2 :

for H being ZF-formula holds variables_in H = (rng H) \ {0,1,2,3,4};

for H being ZF-formula holds variables_in H = (rng H) \ {0,1,2,3,4};

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 )

for a being set st a in variables_in H holds

( a <> 0 & a <> 1 & a <> 2 & a <> 3 & a <> 4 )

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}

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

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}

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}

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}

for x, y, z being Variable holds variables_in (Ex (x,y,z,H)) = (variables_in H) \/ {x,y,z}

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

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

definition

let H be ZF-formula;

let x, y be Variable;

ex b_{1} being Function st

( dom b_{1} = dom H & ( for a being set st a in dom H holds

( ( H . a = x implies b_{1} . a = y ) & ( H . a <> x implies b_{1} . a = H . a ) ) ) )

for b_{1}, b_{2} being Function st dom b_{1} = dom H & ( for a being set st a in dom H holds

( ( H . a = x implies b_{1} . a = y ) & ( H . a <> x implies b_{1} . a = H . a ) ) ) & dom b_{2} = dom H & ( for a being set st a in dom H holds

( ( H . a = x implies b_{2} . a = y ) & ( H . a <> x implies b_{2} . a = H . a ) ) ) holds

b_{1} = b_{2}

end;
let x, y be Variable;

func H / (x,y) -> Function means :Def3: :: ZF_LANG1:def 3

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

ex b

( dom b

( ( H . a = x implies b

proof end;

uniqueness for b

( ( H . a = x implies b

( ( H . a = x implies b

b

proof end;

:: deftheorem Def3 defines / ZF_LANG1:def 3 :

for H being ZF-formula

for x, y being Variable

for b_{4} being Function holds

( b_{4} = H / (x,y) iff ( dom b_{4} = dom H & ( for a being set st a in dom H holds

( ( H . a = x implies b_{4} . a = y ) & ( H . a <> x implies b_{4} . a = H . a ) ) ) ) );

for H being ZF-formula

for x, y being Variable

for b

( b

( ( H . a = x implies b

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

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

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

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;

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

end;
let x, y be Variable;

:: original: /

redefine func H / (x,y) -> ZF-formula;

coherence

H / (x,y) is ZF-formula

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

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 z, x, y being Variable st z <> x holds

( All (z,G) = (All (z,H)) / (x,y) iff G = H / (x,y) )

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

for y, x 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) ) )

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

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

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 z, x, y being Variable st z <> x holds

( Ex (z,G) = (Ex (z,H)) / (x,y) iff G = H / (x,y) )

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

for y, x 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 )

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 )

for x, y being Variable holds

( H is being_membership iff H / (x,y) is being_membership )

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 )

for x, y being Variable holds

( H is conjunctive iff H / (x,y) is conjunctive )

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)

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

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

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 )

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 )

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

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 )

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

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

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

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

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

for x, y being Variable st x in variables_in H holds

y in variables_in (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}

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

proof end;

:: Axioms of Logic

::