:: ZF_LANG1 semantic presentation

theorem Th1: :: ZF_LANG1:1

for b₁, b₂ being Variable holds
( Var1 (b₁ '=' b₂) = b₁ & Var2 (b₁ '=' b₂) = b₂ )

proof end;

theorem Th2: :: ZF_LANG1:2

for b₁, b₂ being Variable holds
( Var1 (b₁ 'in' b₂) = b₁ & Var2 (b₁ 'in' b₂) = b₂ )

proof end;

theorem Th3: :: ZF_LANG1:3

for b₁ being ZF-formula holds the_argument_of ('not' b₁) = b₁

proof end;

theorem Th4: :: ZF_LANG1:4

for b₁, b₂ being ZF-formula holds
( the_left_argument_of (b₁ '&' b₂) = b₁ & the_right_argument_of (b₁ '&' b₂) = b₂ )

proof end;

theorem Th5: :: ZF_LANG1:5

for b₁, b₂ being ZF-formula holds
( the_left_argument_of (b₁ 'or' b₂) = b₁ & the_right_argument_of (b₁ 'or' b₂) = b₂ )

proof end;

theorem Th6: :: ZF_LANG1:6

for b₁, b₂ being ZF-formula holds
( the_antecedent_of (b₁ => b₂) = b₁ & the_consequent_of (b₁ => b₂) = b₂ )

proof end;

theorem Th7: :: ZF_LANG1:7

for b₁, b₂ being ZF-formula holds
( the_left_side_of (b₁ <=> b₂) = b₁ & the_right_side_of (b₁ <=> b₂) = b₂ )

proof end;

theorem Th8: :: ZF_LANG1:8

for b₁ being ZF-formula
for b₂ being Variable holds
( bound_in (All b₂,b₁) = b₂ & the_scope_of (All b₂,b₁) = b₁ )

proof end;

theorem Th9: :: ZF_LANG1:9

for b₁ being ZF-formula
for b₂ being Variable holds
( bound_in (Ex b₂,b₁) = b₂ & the_scope_of (Ex b₂,b₁) = b₁ )

proof end;

theorem Th10: :: ZF_LANG1:10

for b₁, b₂ being ZF-formula holds b₁ 'or' b₂ = ('not' b₁) => b₂ ;

theorem Th11: :: ZF_LANG1:11

for b₁, b₂ being ZF-formula
for b₃, b₄, b₅ being Variable st All b₃,b₄,b₁ = All b₅,b₂ holds
( b₃ = b₅ & All b₄,b₁ = b₂ ) by ZF_LANG:12;

theorem Th12: :: ZF_LANG1:12

for b₁, b₂ being ZF-formula
for b₃, b₄, b₅ being Variable st Ex b₃,b₄,b₁ = Ex b₅,b₂ holds
( b₃ = b₅ & Ex b₄,b₁ = b₂ ) by ZF_LANG:51;

theorem Th13: :: ZF_LANG1:13

for b₁ being ZF-formula
for b₂, b₃ being Variable holds
( All b₂,b₃,b₁ is universal & bound_in (All b₂,b₃,b₁) = b₂ & the_scope_of (All b₂,b₃,b₁) = All b₃,b₁ ) by Th8, ZF_LANG:16;

theorem Th14: :: ZF_LANG1:14

for b₁ being ZF-formula
for b₂, b₃ being Variable holds
( Ex b₂,b₃,b₁ is existential & bound_in (Ex b₂,b₃,b₁) = b₂ & the_scope_of (Ex b₂,b₃,b₁) = Ex b₃,b₁ ) by Th9, ZF_LANG:22;

theorem Th15: :: ZF_LANG1:15

for b₁ being ZF-formula
for b₂, b₃, b₄ being Variable holds
( All b₂,b₃,b₄,b₁ = All b₂,(All b₃,(All b₄,b₁)) & All b₂,b₃,b₄,b₁ = All b₂,b₃,(All b₄,b₁) ) ;

theorem Th16: :: ZF_LANG1:16

for b₁, b₂ being ZF-formula
for b₃, b₄, b₅, b₆ being Variable st All b₃,b₄,b₁ = All b₅,b₆,b₂ holds
( b₃ = b₅ & b₄ = b₆ & b₁ = b₂ )

proof end;

theorem Th17: :: ZF_LANG1:17

for b₁, b₂ being ZF-formula
for b₃, b₄, b₅, b₆, b₇, b₈ being Variable st All b₃,b₄,b₅,b₁ = All b₆,b₇,b₈,b₂ holds
( b₃ = b₆ & b₄ = b₇ & b₅ = b₈ & b₁ = b₂ )

proof end;

theorem Th18: :: ZF_LANG1:18

for b₁, b₂ being ZF-formula
for b₃, b₄, b₅, b₆ being Variable st All b₃,b₄,b₅,b₁ = All b₆,b₂ holds
( b₃ = b₆ & All b₄,b₅,b₁ = b₂ ) by ZF_LANG:12;

theorem Th19: :: ZF_LANG1:19

for b₁, b₂ being ZF-formula
for b₃, b₄, b₅, b₆, b₇ being Variable st All b₃,b₄,b₅,b₁ = All b₆,b₇,b₂ holds
( b₃ = b₆ & b₄ = b₇ & All b₅,b₁ = b₂ )

proof end;

theorem Th20: :: ZF_LANG1:20

for b₁, b₂ being ZF-formula
for b₃, b₄, b₅, b₆ being Variable st Ex b₃,b₄,b₁ = Ex b₅,b₆,b₂ holds
( b₃ = b₅ & b₄ = b₆ & b₁ = b₂ )

proof end;

theorem Th21: :: ZF_LANG1:21

for b₁ being ZF-formula
for b₂, b₃, b₄ being Variable holds
( Ex b₂,b₃,b₄,b₁ = Ex b₂,(Ex b₃,(Ex b₄,b₁)) & Ex b₂,b₃,b₄,b₁ = Ex b₂,b₃,(Ex b₄,b₁) ) ;

theorem Th22: :: ZF_LANG1:22

for b₁, b₂ being ZF-formula
for b₃, b₄, b₅, b₆, b₇, b₈ being Variable st Ex b₃,b₄,b₅,b₁ = Ex b₆,b₇,b₈,b₂ holds
( b₃ = b₆ & b₄ = b₇ & b₅ = b₈ & b₁ = b₂ )

proof end;

theorem Th23: :: ZF_LANG1:23

for b₁, b₂ being ZF-formula
for b₃, b₄, b₅, b₆ being Variable st Ex b₃,b₄,b₅,b₁ = Ex b₆,b₂ holds
( b₃ = b₆ & Ex b₄,b₅,b₁ = b₂ ) by ZF_LANG:51;

theorem Th24: :: ZF_LANG1:24

for b₁, b₂ being ZF-formula
for b₃, b₄, b₅, b₆, b₇ being Variable st Ex b₃,b₄,b₅,b₁ = Ex b₆,b₇,b₂ holds
( b₃ = b₆ & b₄ = b₇ & Ex b₅,b₁ = b₂ )

proof end;

theorem Th25: :: ZF_LANG1:25

for b₁ being ZF-formula
for b₂, b₃, b₄ being Variable holds
( All b₂,b₃,b₄,b₁ is universal & bound_in (All b₂,b₃,b₄,b₁) = b₂ & the_scope_of (All b₂,b₃,b₄,b₁) = All b₃,b₄,b₁ ) by Th8, ZF_LANG:16;

theorem Th26: :: ZF_LANG1:26

for b₁ being ZF-formula
for b₂, b₃, b₄ being Variable holds
( Ex b₂,b₃,b₄,b₁ is existential & bound_in (Ex b₂,b₃,b₄,b₁) = b₂ & the_scope_of (Ex b₂,b₃,b₄,b₁) = Ex b₃,b₄,b₁ ) by Th9, ZF_LANG:22;

theorem Th27: :: ZF_LANG1:27

for b₁ being ZF-formula st b₁ is disjunctive holds
the_left_argument_of b₁ = the_argument_of (the_left_argument_of (the_argument_of b₁))

proof end;

theorem Th28: :: ZF_LANG1:28

for b₁ being ZF-formula st b₁ is disjunctive holds
the_right_argument_of b₁ = the_argument_of (the_right_argument_of (the_argument_of b₁))

proof end;

theorem Th29: :: ZF_LANG1:29

for b₁ being ZF-formula st b₁ is conditional holds
the_antecedent_of b₁ = the_left_argument_of (the_argument_of b₁)

proof end;

theorem Th30: :: ZF_LANG1:30

for b₁ being ZF-formula st b₁ is conditional holds
the_consequent_of b₁ = the_argument_of (the_right_argument_of (the_argument_of b₁))

proof end;

theorem Th31: :: ZF_LANG1:31

for b₁ being ZF-formula st b₁ is biconditional holds
( the_left_side_of b₁ = the_antecedent_of (the_left_argument_of b₁) & the_left_side_of b₁ = the_consequent_of (the_right_argument_of b₁) )

proof end;

theorem Th32: :: ZF_LANG1:32

for b₁ being ZF-formula st b₁ is biconditional holds
( the_right_side_of b₁ = the_consequent_of (the_left_argument_of b₁) & the_right_side_of b₁ = the_antecedent_of (the_right_argument_of b₁) )

proof end;

theorem Th33: :: ZF_LANG1:33

for b₁ being ZF-formula st b₁ is existential holds
( bound_in b₁ = bound_in (the_argument_of b₁) & the_scope_of b₁ = the_argument_of (the_scope_of (the_argument_of b₁)) )

proof end;

theorem Th34: :: ZF_LANG1:34

for b₁, b₂ being ZF-formula holds
( the_argument_of (b₁ 'or' b₂) = ('not' b₁) '&' ('not' b₂) & the_antecedent_of (b₁ 'or' b₂) = 'not' b₁ & the_consequent_of (b₁ 'or' b₂) = b₂ )

proof end;

theorem Th35: :: ZF_LANG1:35

for b₁, b₂ being ZF-formula holds the_argument_of (b₁ => b₂) = b₁ '&' ('not' b₂) by Th3;

theorem Th36: :: ZF_LANG1:36

for b₁, b₂ being ZF-formula holds
( the_left_argument_of (b₁ <=> b₂) = b₁ => b₂ & the_right_argument_of (b₁ <=> b₂) = b₂ => b₁ ) by Th4;

theorem Th37: :: ZF_LANG1:37

for b₁ being ZF-formula
for b₂ being Variable holds the_argument_of (Ex b₂,b₁) = All b₂,('not' b₁) by Th3;

theorem Th38: :: ZF_LANG1:38

for b₁ being ZF-formula st b₁ is disjunctive holds
( b₁ is conditional & b₁ is negative & the_argument_of b₁ is conjunctive & the_left_argument_of (the_argument_of b₁) is negative & the_right_argument_of (the_argument_of b₁) is negative )

proof end;

theorem Th39: :: ZF_LANG1:39

for b₁ being ZF-formula st b₁ is conditional holds
( b₁ is negative & the_argument_of b₁ is conjunctive & the_right_argument_of (the_argument_of b₁) is negative )

proof end;

theorem Th40: :: ZF_LANG1:40

for b₁ being ZF-formula st b₁ is biconditional holds
( b₁ is conjunctive & the_left_argument_of b₁ is conditional & the_right_argument_of b₁ is conditional )

proof end;

theorem Th41: :: ZF_LANG1:41

for b₁ being ZF-formula st b₁ is existential holds
( b₁ is negative & the_argument_of b₁ is universal & the_scope_of (the_argument_of b₁) is negative )

proof end;

theorem Th42: :: ZF_LANG1:42

for b₁ being ZF-formula holds
( ( not b₁ is_equality or ( not b₁ is_membership & not b₁ is negative & not b₁ is conjunctive & not b₁ is universal ) ) & ( not b₁ is_membership or ( not b₁ is negative & not b₁ is conjunctive & not b₁ is universal ) ) & ( not b₁ is negative or ( not b₁ is conjunctive & not b₁ is universal ) ) & ( not b₁ is conjunctive or not b₁ is universal ) )

proof end;

theorem Th43: :: ZF_LANG1:43

for b₁, b₂ being ZF-formula st b₁ is_subformula_of b₂ holds
len b₁ <= len b₂

proof end;

theorem Th44: :: ZF_LANG1:44

for b₁, b₂, b₃ being ZF-formula st ( ( b₁ is_proper_subformula_of b₂ & b₂ is_subformula_of b₃ ) or ( b₁ is_subformula_of b₂ & b₂ is_proper_subformula_of b₃ ) or ( b₁ is_subformula_of b₂ & b₂ is_immediate_constituent_of b₃ ) or ( b₁ is_immediate_constituent_of b₂ & b₂ is_subformula_of b₃ ) or ( b₁ is_proper_subformula_of b₂ & b₂ is_immediate_constituent_of b₃ ) or ( b₁ is_immediate_constituent_of b₂ & b₂ is_proper_subformula_of b₃ ) ) holds
b₁ is_proper_subformula_of b₃

proof end;

theorem Th45: :: ZF_LANG1:45

canceled;

theorem Th46: :: ZF_LANG1:46

for b₁ being ZF-formula holds not b₁ is_immediate_constituent_of b₁

proof end;

theorem Th47: :: ZF_LANG1:47

for b₁, b₂ being ZF-formula holds
( not b₁ is_proper_subformula_of b₂ or not b₂ is_subformula_of b₁ )

proof end;

theorem Th48: :: ZF_LANG1:48

for b₁, b₂ being ZF-formula holds
( not b₁ is_proper_subformula_of b₂ or not b₂ is_proper_subformula_of b₁ )

proof end;

theorem Th49: :: ZF_LANG1:49

for b₁, b₂ being ZF-formula holds
( not b₁ is_subformula_of b₂ or not b₂ is_immediate_constituent_of b₁ )

proof end;

theorem Th50: :: ZF_LANG1:50

for b₁, b₂ being ZF-formula holds
( not b₁ is_proper_subformula_of b₂ or not b₂ is_immediate_constituent_of b₁ )

proof end;

theorem Th51: :: ZF_LANG1:51

for b₁, b₂ being ZF-formula st 'not' b₁ is_subformula_of b₂ holds
b₁ is_proper_subformula_of b₂

proof end;

theorem Th52: :: ZF_LANG1:52

for b₁, b₂, b₃ being ZF-formula st b₁ '&' b₂ is_subformula_of b₃ holds
( b₁ is_proper_subformula_of b₃ & b₂ is_proper_subformula_of b₃ )

proof end;

theorem Th53: :: ZF_LANG1:53

for b₁, b₂ being ZF-formula
for b₃ being Variable st All b₃,b₁ is_subformula_of b₂ holds
b₁ is_proper_subformula_of b₂

proof end;

theorem Th54: :: ZF_LANG1:54

for b₁, b₂ being ZF-formula holds
( b₁ '&' ('not' b₂) is_proper_subformula_of b₁ => b₂ & b₁ is_proper_subformula_of b₁ => b₂ & 'not' b₂ is_proper_subformula_of b₁ => b₂ & b₂ is_proper_subformula_of b₁ => b₂ )

proof end;

theorem Th55: :: ZF_LANG1:55

for b₁, b₂ being ZF-formula holds
( ('not' b₁) '&' ('not' b₂) is_proper_subformula_of b₁ 'or' b₂ & 'not' b₁ is_proper_subformula_of b₁ 'or' b₂ & 'not' b₂ is_proper_subformula_of b₁ 'or' b₂ & b₁ is_proper_subformula_of b₁ 'or' b₂ & b₂ is_proper_subformula_of b₁ 'or' b₂ )

proof end;

theorem Th56: :: ZF_LANG1:56

for b₁ being ZF-formula
for b₂ being Variable holds
( All b₂,('not' b₁) is_proper_subformula_of Ex b₂,b₁ & 'not' b₁ is_proper_subformula_of Ex b₂,b₁ )

proof end;

theorem Th57: :: ZF_LANG1:57

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

theorem Th58: :: ZF_LANG1:58

for b₁, b₂ being ZF-formula st b₁ in Subformulae b₂ holds
Subformulae b₁ c= Subformulae b₂

proof end;

theorem Th59: :: ZF_LANG1:59

for b₁ being ZF-formula holds b₁ in Subformulae b₁

proof end;

theorem Th60: :: ZF_LANG1:60

for b₁, b₂ being ZF-formula holds Subformulae (b₁ => b₂) = ((Subformulae b₁) \/ (Subformulae b₂)) \/ {('not' b₂),(b₁ '&' ('not' b₂)),(b₁ => b₂)}

proof end;

theorem Th61: :: ZF_LANG1:61

for b₁, b₂ being ZF-formula holds Subformulae (b₁ 'or' b₂) = ((Subformulae b₁) \/ (Subformulae b₂)) \/ {('not' b₂),('not' b₁),(('not' b₁) '&' ('not' b₂)),(b₁ 'or' b₂)}

proof end;

theorem Th62: :: ZF_LANG1:62

for b₁, b₂ being ZF-formula holds Subformulae (b₁ <=> b₂) = ((Subformulae b₁) \/ (Subformulae b₂)) \/ {('not' b₂),(b₁ '&' ('not' b₂)),(b₁ => b₂),('not' b₁),(b₂ '&' ('not' b₁)),(b₂ => b₁),(b₁ <=> b₂)}

proof end;

theorem Th63: :: ZF_LANG1:63

for b₁, b₂ being Variable holds Free (b₁ '=' b₂) = {b₁,b₂}

proof end;

theorem Th64: :: ZF_LANG1:64

for b₁, b₂ being Variable holds Free (b₁ 'in' b₂) = {b₁,b₂}

proof end;

theorem Th65: :: ZF_LANG1:65

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

proof end;

theorem Th66: :: ZF_LANG1:66

for b₁, b₂ being ZF-formula holds Free (b₁ '&' b₂) = (Free b₁) \/ (Free b₂)

proof end;

theorem Th67: :: ZF_LANG1:67

for b₁ being ZF-formula
for b₂ being Variable holds Free (All b₂,b₁) = (Free b₁) \ {b₂}

proof end;

theorem Th68: :: ZF_LANG1:68

for b₁, b₂ being ZF-formula holds Free (b₁ 'or' b₂) = (Free b₁) \/ (Free b₂)

proof end;

theorem Th69: :: ZF_LANG1:69

for b₁, b₂ being ZF-formula holds Free (b₁ => b₂) = (Free b₁) \/ (Free b₂)

proof end;

theorem Th70: :: ZF_LANG1:70

for b₁, b₂ being ZF-formula holds Free (b₁ <=> b₂) = (Free b₁) \/ (Free b₂)

proof end;

theorem Th71: :: ZF_LANG1:71

for b₁ being ZF-formula
for b₂ being Variable holds Free (Ex b₂,b₁) = (Free b₁) \ {b₂}

proof end;

theorem Th72: :: ZF_LANG1:72

for b₁ being ZF-formula
for b₂, b₃ being Variable holds Free (All b₂,b₃,b₁) = (Free b₁) \ {b₂,b₃}

proof end;

theorem Th73: :: ZF_LANG1:73

for b₁ being ZF-formula
for b₂, b₃, b₄ being Variable holds Free (All b₂,b₃,b₄,b₁) = (Free b₁) \ {b₂,b₃,b₄}

proof end;

theorem Th74: :: ZF_LANG1:74

for b₁ being ZF-formula
for b₂, b₃ being Variable holds Free (Ex b₂,b₃,b₁) = (Free b₁) \ {b₂,b₃}

proof end;

theorem Th75: :: ZF_LANG1:75

for b₁ being ZF-formula
for b₂, b₃, b₄ being Variable holds Free (Ex b₂,b₃,b₄,b₁) = (Free b₁) \ {b₂,b₃,b₄}

proof end;

scheme :: ZF_LANG1:sch 1
s1{ P₁[ ZF-formula] } :

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

provided

E22: for b₁, b₂ being Variable holds
( P₁[b₁ '=' b₂] & P₁[b₁ 'in' b₂] ) and
E23: for b₁ being ZF-formula st P₁[b₁] holds
P₁[ 'not' b₁] and
E24: for b₁, b₂ being ZF-formula st P₁[b₁] & P₁[b₂] holds
P₁[b₁ '&' b₂] and
E25: for b₁ being ZF-formula
for b₂ being Variable st P₁[b₁] holds
P₁[ All b₂,b₁]

proof end;

definition

let c₁ be non empty set ;
let c₂ be Function of VAR ,c₁;
let c₃ be Variable;
let c₄ be Element of c₁;
func c₂ / c₃,c₄ -> Function of VAR ,a₁ means :Def1: :: ZF_LANG1:def 1
( a₅ . a₃ = a₄ & ( for b₁ being Variable st a₅ . b₁ <> a₂ . b₁ holds
a₃ = b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines / ZF_LANG1:def 1 :

definition

let c₁, c₂, c₃ be non empty set ;
let c₄ be Function of c₁,c₂;
assume E23: c₂ c= c₃ ;
func c₃ ! c₄ -> Function of a₁,a₃ equals :: ZF_LANG1:def 2
a₄;
correctness

proof end;

end;

:: deftheorem Def2 defines ! ZF_LANG1:def 2 :

theorem Th76: :: ZF_LANG1:76

canceled;

theorem Th77: :: ZF_LANG1:77

canceled;

theorem Th78: :: ZF_LANG1:78

for b₁ being Variable
for b₂ being non empty set
for b₃, b₄ being Element of b₂
for b₅ being Function of VAR ,b₂ holds
( (b₅ / b₁,b₃) / b₁,b₄ = b₅ / b₁,b₄ & b₅ / b₁,(b₅ . b₁) = b₅ )

proof end;

theorem Th79: :: ZF_LANG1:79

for b₁, b₂ being Variable
for b₃ being non empty set
for b₄, b₅ being Element of b₃
for b₆ being Function of VAR ,b₃ st b₁ <> b₂ holds
(b₆ / b₁,b₄) / b₂,b₅ = (b₆ / b₂,b₅) / b₁,b₄

proof end;

theorem Th80: :: ZF_LANG1:80

for b₁ being ZF-formula
for b₂ being Variable
for b₃ being non empty set
for b₄ being Function of VAR ,b₃ holds
( b₃,b₄ |= All b₂,b₁ iff for b₅ being Element of b₃ holds b₃,b₄ / b₂,b₅ |= b₁ )

proof end;

theorem Th81: :: ZF_LANG1:81

for b₁ being ZF-formula
for b₂ being Variable
for b₃ being non empty set
for b₄ being Element of b₃
for b₅ being Function of VAR ,b₃ holds
( b₃,b₅ |= All b₂,b₁ iff b₃,b₅ / b₂,b₄ |= All b₂,b₁ )

proof end;

theorem Th82: :: ZF_LANG1:82

for b₁ being ZF-formula
for b₂ being Variable
for b₃ being non empty set
for b₄ being Function of VAR ,b₃ holds
( b₃,b₄ |= Ex b₂,b₁ iff ex b₅ being Element of b₃ st b₃,b₄ / b₂,b₅ |= b₁ )

proof end;

theorem Th83: :: ZF_LANG1:83

for b₁ being ZF-formula
for b₂ being Variable
for b₃ being non empty set
for b₄ being Element of b₃
for b₅ being Function of VAR ,b₃ holds
( b₃,b₅ |= Ex b₂,b₁ iff b₃,b₅ / b₂,b₄ |= Ex b₂,b₁ )

proof end;

theorem Th84: :: ZF_LANG1:84

for b₁ being ZF-formula
for b₂ being non empty set
for b₃, b₄ being Function of VAR ,b₂ st ( for b₅ being Variable st b₅ in Free b₁ holds
b₄ . b₅ = b₃ . b₅ ) & b₂,b₃ |= b₁ holds
b₂,b₄ |= b₁

proof end;

theorem Th85: :: ZF_LANG1:85

for b₁ being ZF-formula holds Free b₁ is finite

proof end;

registration

let c₁ be ZF-formula;
cluster Free a₁ -> finite ;
coherence by Th85;

end;

theorem Th86: :: ZF_LANG1:86

for b₁, b₂ being Nat st x. b₁ = x. b₂ holds
b₁ = b₂ by XCMPLX_1:2;

theorem Th87: :: ZF_LANG1:87

for b₁ being Variable ex b₂ being Nat st b₁ = x. b₂

proof end;

theorem Th88: :: ZF_LANG1:88

canceled;

theorem Th89: :: ZF_LANG1:89

for b₁ being Variable
for b₂ being non empty set
for b₃ being Function of VAR ,b₂ holds b₂,b₃ |= b₁ '=' b₁

proof end;

theorem Th90: :: ZF_LANG1:90

for b₁ being Variable
for b₂ being non empty set holds b₂ |= b₁ '=' b₁

proof end;

theorem Th91: :: ZF_LANG1:91

for b₁ being Variable
for b₂ being non empty set
for b₃ being Function of VAR ,b₂ holds not b₂,b₃ |= b₁ 'in' b₁

proof end;

theorem Th92: :: ZF_LANG1:92

for b₁ being Variable
for b₂ being non empty set holds
( not b₂ |= b₁ 'in' b₁ & b₂ |= 'not' (b₁ 'in' b₁) )

proof end;

theorem Th93: :: ZF_LANG1:93

for b₁, b₂ being Variable
for b₃ being non empty set holds
( b₃ |= b₁ '=' b₂ iff ( b₁ = b₂ or ex b₄ being set st {b₄} = b₃ ) )

proof end;

theorem Th94: :: ZF_LANG1:94

for b₁, b₂ being Variable
for b₃ being non empty set holds
( b₃ |= 'not' (b₁ 'in' b₂) iff ( b₁ = b₂ or for b₄ being set st b₄ in b₃ holds
b₄ misses b₃ ) )

proof end;

theorem Th95: :: ZF_LANG1:95

for b₁ being ZF-formula
for b₂ being non empty set
for b₃ being Function of VAR ,b₂ st b₁ is_equality holds
( b₂,b₃ |= b₁ iff b₃ . (Var1 b₁) = b₃ . (Var2 b₁) )

proof end;

theorem Th96: :: ZF_LANG1:96

for b₁ being ZF-formula
for b₂ being non empty set
for b₃ being Function of VAR ,b₂ st b₁ is_membership holds
( b₂,b₃ |= b₁ iff b₃ . (Var1 b₁) in b₃ . (Var2 b₁) )

proof end;

theorem Th97: :: ZF_LANG1:97

for b₁ being ZF-formula
for b₂ being non empty set
for b₃ being Function of VAR ,b₂ st b₁ is negative holds
( b₂,b₃ |= b₁ iff not b₂,b₃ |= the_argument_of b₁ )

proof end;

theorem Th98: :: ZF_LANG1:98

for b₁ being ZF-formula
for b₂ being non empty set
for b₃ being Function of VAR ,b₂ st b₁ is conjunctive holds
( b₂,b₃ |= b₁ iff ( b₂,b₃ |= the_left_argument_of b₁ & b₂,b₃ |= the_right_argument_of b₁ ) )

proof end;

theorem Th99: :: ZF_LANG1:99

for b₁ being ZF-formula
for b₂ being non empty set
for b₃ being Function of VAR ,b₂ st b₁ is universal holds
( b₂,b₃ |= b₁ iff for b₄ being Element of b₂ holds b₂,b₃ / (bound_in b₁),b₄ |= the_scope_of b₁ )

proof end;

theorem Th100: :: ZF_LANG1:100

for b₁ being ZF-formula
for b₂ being non empty set
for b₃ being Function of VAR ,b₂ st b₁ is disjunctive holds
( b₂,b₃ |= b₁ iff ( b₂,b₃ |= the_left_argument_of b₁ or b₂,b₃ |= the_right_argument_of b₁ ) )

proof end;

theorem Th101: :: ZF_LANG1:101

for b₁ being ZF-formula
for b₂ being non empty set
for b₃ being Function of VAR ,b₂ st b₁ is conditional holds
( b₂,b₃ |= b₁ iff ( b₂,b₃ |= the_antecedent_of b₁ implies b₂,b₃ |= the_consequent_of b₁ ) )

proof end;

theorem Th102: :: ZF_LANG1:102

for b₁ being ZF-formula
for b₂ being non empty set
for b₃ being Function of VAR ,b₂ st b₁ is biconditional holds
( b₂,b₃ |= b₁ iff ( b₂,b₃ |= the_left_side_of b₁ iff b₂,b₃ |= the_right_side_of b₁ ) )

proof end;

theorem Th103: :: ZF_LANG1:103

for b₁ being ZF-formula
for b₂ being non empty set
for b₃ being Function of VAR ,b₂ st b₁ is existential holds
( b₂,b₃ |= b₁ iff ex b₄ being Element of b₂ st b₂,b₃ / (bound_in b₁),b₄ |= the_scope_of b₁ )

proof end;

theorem Th104: :: ZF_LANG1:104

for b₁ being ZF-formula
for b₂ being Variable
for b₃ being non empty set holds
( b₃ |= Ex b₂,b₁ iff for b₄ being Function of VAR ,b₃ ex b₅ being Element of b₃ st b₃,b₄ / b₂,b₅ |= b₁ )

proof end;

theorem Th105: :: ZF_LANG1:105

for b₁ being ZF-formula
for b₂ being Variable
for b₃ being non empty set st b₃ |= b₁ holds
b₃ |= Ex b₂,b₁

proof end;

theorem Th106: :: ZF_LANG1:106

for b₁ being ZF-formula
for b₂, b₃ being Variable
for b₄ being non empty set holds
( b₄ |= b₁ iff b₄ |= All b₂,b₃,b₁ )

proof end;

theorem Th107: :: ZF_LANG1:107

for b₁ being ZF-formula
for b₂, b₃ being Variable
for b₄ being non empty set st b₄ |= b₁ holds
b₄ |= Ex b₂,b₃,b₁

proof end;

theorem Th108: :: ZF_LANG1:108

for b₁ being ZF-formula
for b₂, b₃, b₄ being Variable
for b₅ being non empty set holds
( b₅ |= b₁ iff b₅ |= All b₂,b₃,b₄,b₁ )

proof end;

theorem Th109: :: ZF_LANG1:109

for b₁ being ZF-formula
for b₂, b₃, b₄ being Variable
for b₅ being non empty set st b₅ |= b₁ holds
b₅ |= Ex b₂,b₃,b₄,b₁

proof end;

theorem Th110: :: ZF_LANG1:110

for b₁, b₂ being ZF-formula
for b₃ being non empty set
for b₄ being Function of VAR ,b₃ holds
( b₃,b₄ |= (b₁ <=> b₂) => (b₁ => b₂) & b₃ |= (b₁ <=> b₂) => (b₁ => b₂) )

proof end;

theorem Th111: :: ZF_LANG1:111

for b₁, b₂ being ZF-formula
for b₃ being non empty set
for b₄ being Function of VAR ,b₃ holds
( b₃,b₄ |= (b₁ <=> b₂) => (b₂ => b₁) & b₃ |= (b₁ <=> b₂) => (b₂ => b₁) )

proof end;

theorem Th112: :: ZF_LANG1:112

for b₁, b₂, b₃ being ZF-formula
for b₄ being non empty set holds b₄ |= (b₁ => b₂) => ((b₂ => b₃) => (b₁ => b₃))

proof end;

theorem Th113: :: ZF_LANG1:113

for b₁, b₂, b₃ being ZF-formula
for b₄ being non empty set
for b₅ being Function of VAR ,b₄ st b₄,b₅ |= b₁ => b₂ & b₄,b₅ |= b₂ => b₃ holds
b₄,b₅ |= b₁ => b₃

proof end;

theorem Th114: :: ZF_LANG1:114

for b₁, b₂, b₃ being ZF-formula
for b₄ being non empty set st b₄ |= b₁ => b₂ & b₄ |= b₂ => b₃ holds
b₄ |= b₁ => b₃

proof end;

theorem Th115: :: ZF_LANG1:115

for b₁, b₂, b₃ being ZF-formula
for b₄ being non empty set
for b₅ being Function of VAR ,b₄ holds
( b₄,b₅ |= ((b₁ => b₂) '&' (b₂ => b₃)) => (b₁ => b₃) & b₄ |= ((b₁ => b₂) '&' (b₂ => b₃)) => (b₁ => b₃) )

proof end;

theorem Th116: :: ZF_LANG1:116

for b₁, b₂ being ZF-formula
for b₃ being non empty set
for b₄ being Function of VAR ,b₃ holds
( b₃,b₄ |= b₁ => (b₂ => b₁) & b₃ |= b₁ => (b₂ => b₁) )

proof end;

theorem Th117: :: ZF_LANG1:117

for b₁, b₂, b₃ being ZF-formula
for b₄ being non empty set
for b₅ being Function of VAR ,b₄ holds
( b₄,b₅ |= (b₁ => (b₂ => b₃)) => ((b₁ => b₂) => (b₁ => b₃)) & b₄ |= (b₁ => (b₂ => b₃)) => ((b₁ => b₂) => (b₁ => b₃)) )

proof end;

theorem Th118: :: ZF_LANG1:118

for b₁, b₂ being ZF-formula
for b₃ being non empty set
for b₄ being Function of VAR ,b₃ holds
( b₃,b₄ |= (b₁ '&' b₂) => b₁ & b₃ |= (b₁ '&' b₂) => b₁ )

proof end;

theorem Th119: :: ZF_LANG1:119

for b₁, b₂ being ZF-formula
for b₃ being non empty set
for b₄ being Function of VAR ,b₃ holds
( b₃,b₄ |= (b₁ '&' b₂) => b₂ & b₃ |= (b₁ '&' b₂) => b₂ )

proof end;

theorem Th120: :: ZF_LANG1:120

for b₁, b₂ being ZF-formula
for b₃ being non empty set
for b₄ being Function of VAR ,b₃ holds
( b₃,b₄ |= (b₁ '&' b₂) => (b₂ '&' b₁) & b₃ |= (b₁ '&' b₂) => (b₂ '&' b₁) )

proof end;

theorem Th121: :: ZF_LANG1:121

for b₁ being ZF-formula
for b₂ being non empty set
for b₃ being Function of VAR ,b₂ holds
( b₂,b₃ |= b₁ => (b₁ '&' b₁) & b₂ |= b₁ => (b₁ '&' b₁) )

proof end;

theorem Th122: :: ZF_LANG1:122

for b₁, b₂, b₃ being ZF-formula
for b₄ being non empty set
for b₅ being Function of VAR ,b₄ holds
( b₄,b₅ |= (b₁ => b₂) => ((b₁ => b₃) => (b₁ => (b₂ '&' b₃))) & b₄ |= (b₁ => b₂) => ((b₁ => b₃) => (b₁ => (b₂ '&' b₃))) )

proof end;

theorem Th123: :: ZF_LANG1:123

for b₁, b₂ being ZF-formula
for b₃ being non empty set
for b₄ being Function of VAR ,b₃ holds
( b₃,b₄ |= b₁ => (b₁ 'or' b₂) & b₃ |= b₁ => (b₁ 'or' b₂) )

proof end;

theorem Th124: :: ZF_LANG1:124

for b₁, b₂ being ZF-formula
for b₃ being non empty set
for b₄ being Function of VAR ,b₃ holds
( b₃,b₄ |= b₁ => (b₂ 'or' b₁) & b₃ |= b₁ => (b₂ 'or' b₁) )

proof end;

theorem Th125: :: ZF_LANG1:125

for b₁, b₂ being ZF-formula
for b₃ being non empty set
for b₄ being Function of VAR ,b₃ holds
( b₃,b₄ |= (b₁ 'or' b₂) => (b₂ 'or' b₁) & b₃ |= (b₁ 'or' b₂) => (b₂ 'or' b₁) )

proof end;

theorem Th126: :: ZF_LANG1:126

for b₁ being ZF-formula
for b₂ being non empty set
for b₃ being Function of VAR ,b₂ holds
( b₂,b₃ |= b₁ => (b₁ 'or' b₁) & b₂ |= b₁ => (b₁ 'or' b₁) ) by Th123;

theorem Th127: :: ZF_LANG1:127

for b₁, b₂, b₃ being ZF-formula
for b₄ being non empty set
for b₅ being Function of VAR ,b₄ holds
( b₄,b₅ |= (b₁ => b₂) => ((b₃ => b₂) => ((b₁ 'or' b₃) => b₂)) & b₄ |= (b₁ => b₂) => ((b₃ => b₂) => ((b₁ 'or' b₃) => b₂)) )

proof end;

theorem Th128: :: ZF_LANG1:128

for b₁, b₂, b₃ being ZF-formula
for b₄ being non empty set
for b₅ being Function of VAR ,b₄ holds
( b₄,b₅ |= ((b₁ => b₂) '&' (b₃ => b₂)) => ((b₁ 'or' b₃) => b₂) & b₄ |= ((b₁ => b₂) '&' (b₃ => b₂)) => ((b₁ 'or' b₃) => b₂) )

proof end;

theorem Th129: :: ZF_LANG1:129

for b₁, b₂ being ZF-formula
for b₃ being non empty set
for b₄ being Function of VAR ,b₃ holds
( b₃,b₄ |= (b₁ => ('not' b₂)) => (b₂ => ('not' b₁)) & b₃ |= (b₁ => ('not' b₂)) => (b₂ => ('not' b₁)) )

proof end;

theorem Th130: :: ZF_LANG1:130

for b₁, b₂ being ZF-formula
for b₃ being non empty set
for b₄ being Function of VAR ,b₃ holds
( b₃,b₄ |= ('not' b₁) => (b₁ => b₂) & b₃ |= ('not' b₁) => (b₁ => b₂) )

proof end;

theorem Th131: :: ZF_LANG1:131

for b₁, b₂ being ZF-formula
for b₃ being non empty set
for b₄ being Function of VAR ,b₃ holds
( b₃,b₄ |= ((b₁ => b₂) '&' (b₁ => ('not' b₂))) => ('not' b₁) & b₃ |= ((b₁ => b₂) '&' (b₁ => ('not' b₂))) => ('not' b₁) )

proof end;

theorem Th132: :: ZF_LANG1:132

canceled;

theorem Th133: :: ZF_LANG1:133

for b₁, b₂ being ZF-formula
for b₃ being non empty set st b₃ |= b₁ => b₂ & b₃ |= b₁ holds
b₃ |= b₂

proof end;

theorem Th134: :: ZF_LANG1:134

for b₁, b₂ being ZF-formula
for b₃ being non empty set
for b₄ being Function of VAR ,b₃ holds
( b₃,b₄ |= ('not' (b₁ '&' b₂)) => (('not' b₁) 'or' ('not' b₂)) & b₃ |= ('not' (b₁ '&' b₂)) => (('not' b₁) 'or' ('not' b₂)) )

proof end;

theorem Th135: :: ZF_LANG1:135

for b₁, b₂ being ZF-formula
for b₃ being non empty set
for b₄ being Function of VAR ,b₃ holds
( b₃,b₄ |= (('not' b₁) 'or' ('not' b₂)) => ('not' (b₁ '&' b₂)) & b₃ |= (('not' b₁) 'or' ('not' b₂)) => ('not' (b₁ '&' b₂)) )

proof end;

theorem Th136: :: ZF_LANG1:136

for b₁, b₂ being ZF-formula
for b₃ being non empty set
for b₄ being Function of VAR ,b₃ holds
( b₃,b₄ |= ('not' (b₁ 'or' b₂)) => (('not' b₁) '&' ('not' b₂)) & b₃ |= ('not' (b₁ 'or' b₂)) => (('not' b₁) '&' ('not' b₂)) )

proof end;

theorem Th137: :: ZF_LANG1:137

for b₁, b₂ being ZF-formula
for b₃ being non empty set
for b₄ being Function of VAR ,b₃ holds
( b₃,b₄ |= (('not' b₁) '&' ('not' b₂)) => ('not' (b₁ 'or' b₂)) & b₃ |= (('not' b₁) '&' ('not' b₂)) => ('not' (b₁ 'or' b₂)) )

proof end;

theorem Th138: :: ZF_LANG1:138

for b₁ being ZF-formula
for b₂ being Variable
for b₃ being non empty set holds b₃ |= (All b₂,b₁) => b₁

proof end;

theorem Th139: :: ZF_LANG1:139

for b₁ being ZF-formula
for b₂ being Variable
for b₃ being non empty set holds b₃ |= b₁ => (Ex b₂,b₁)

proof end;

theorem Th140: :: ZF_LANG1:140

for b₁, b₂ being ZF-formula
for b₃ being Variable
for b₄ being non empty set st not b₃ in Free b₁ holds
b₄ |= (All b₃,(b₁ => b₂)) => (b₁ => (All b₃,b₂))

proof end;

theorem Th141: :: ZF_LANG1:141

for b₁, b₂ being ZF-formula
for b₃ being Variable
for b₄ being non empty set st not b₃ in Free b₁ & b₄ |= b₁ => b₂ holds
b₄ |= b₁ => (All b₃,b₂)

proof end;

theorem Th142: :: ZF_LANG1:142

for b₁, b₂ being ZF-formula
for b₃ being Variable
for b₄ being non empty set st not b₃ in Free b₁ holds
b₄ |= (All b₃,(b₂ => b₁)) => ((Ex b₃,b₂) => b₁)

proof end;

theorem Th143: :: ZF_LANG1:143

for b₁, b₂ being ZF-formula
for b₃ being Variable
for b₄ being non empty set st not b₃ in Free b₁ & b₄ |= b₂ => b₁ holds
b₄ |= (Ex b₃,b₂) => b₁

proof end;

theorem Th144: :: ZF_LANG1:144

for b₁, b₂ being ZF-formula
for b₃ being Variable
for b₄ being non empty set st b₄ |= b₁ => (All b₃,b₂) holds
b₄ |= b₁ => b₂

proof end;

theorem Th145: :: ZF_LANG1:145

for b₁, b₂ being ZF-formula
for b₃ being Variable
for b₄ being non empty set st b₄ |= (Ex b₃,b₁) => b₂ holds
b₄ |= b₁ => b₂

proof end;

theorem Th146: :: ZF_LANG1:146

WFF c= bool [:NAT ,NAT :]

proof end;

definition

let c₁ be ZF-formula;
func variables_in c₁ -> set equals :: ZF_LANG1:def 3
(rng a₁) \ {0,1,2,3,4};
correctness ;

end;

:: deftheorem Def3 defines variables_in ZF_LANG1:def 3 :

theorem Th147: :: ZF_LANG1:147

canceled;

theorem Th148: :: ZF_LANG1:148

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

proof end;

theorem Th149: :: ZF_LANG1:149

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

proof end;

theorem Th150: :: ZF_LANG1:150

for b₁ being ZF-formula
for b₂ being set st b₂ in variables_in b₁ holds
( b₂ <> 0 & b₂ <> 1 & b₂ <> 2 & b₂ <> 3 & b₂ <> 4 )

proof end;

theorem Th151: :: ZF_LANG1:151

for b₁, b₂ being Variable holds variables_in (b₁ '=' b₂) = {b₁,b₂}

proof end;

theorem Th152: :: ZF_LANG1:152

for b₁, b₂ being Variable holds variables_in (b₁ 'in' b₂) = {b₁,b₂}

proof end;

theorem Th153: :: ZF_LANG1:153

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

proof end;

theorem Th154: :: ZF_LANG1:154

for b₁, b₂ being ZF-formula holds variables_in (b₁ '&' b₂) = (variables_in b₁) \/ (variables_in b₂)

proof end;

theorem Th155: :: ZF_LANG1:155

for b₁ being ZF-formula
for b₂ being Variable holds variables_in (All b₂,b₁) = (variables_in b₁) \/ {b₂}

proof end;

theorem Th156: :: ZF_LANG1:156

for b₁, b₂ being ZF-formula holds variables_in (b₁ 'or' b₂) = (variables_in b₁) \/ (variables_in b₂)

proof end;

theorem Th157: :: ZF_LANG1:157

for b₁, b₂ being ZF-formula holds variables_in (b₁ => b₂) = (variables_in b₁) \/ (variables_in b₂)

proof end;

theorem Th158: :: ZF_LANG1:158

for b₁, b₂ being ZF-formula holds variables_in (b₁ <=> b₂) = (variables_in b₁) \/ (variables_in b₂)

proof end;

theorem Th159: :: ZF_LANG1:159

for b₁ being ZF-formula
for b₂ being Variable holds variables_in (Ex b₂,b₁) = (variables_in b₁) \/ {b₂}

proof end;

theorem Th160: :: ZF_LANG1:160

for b₁ being ZF-formula
for b₂, b₃ being Variable holds variables_in (All b₂,b₃,b₁) = (variables_in b₁) \/ {b₂,b₃}

proof end;

theorem Th161: :: ZF_LANG1:161

for b₁ being ZF-formula
for b₂, b₃ being Variable holds variables_in (Ex b₂,b₃,b₁) = (variables_in b₁) \/ {b₂,b₃}

proof end;

theorem Th162: :: ZF_LANG1:162

for b₁ being ZF-formula
for b₂, b₃, b₄ being Variable holds variables_in (All b₂,b₃,b₄,b₁) = (variables_in b₁) \/ {b₂,b₃,b₄}

proof end;

theorem Th163: :: ZF_LANG1:163

for b₁ being ZF-formula
for b₂, b₃, b₄ being Variable holds variables_in (Ex b₂,b₃,b₄,b₁) = (variables_in b₁) \/ {b₂,b₃,b₄}

proof end;

theorem Th164: :: ZF_LANG1:164

for b₁ being ZF-formula holds Free b₁ c= variables_in b₁

proof end;

definition

let c₁ be ZF-formula;
redefine func variables_in as variables_in c₁ -> non empty Subset of VAR ;
coherence

proof end;

end;

definition

let c₁ be ZF-formula;
let c₂, c₃ be Variable;
func c₁ / c₂,c₃ -> Function means :Def4: :: ZF_LANG1:def 4
( dom a₄ = dom a₁ & ( for b₁ being set st b₁ in dom a₁ holds
( ( a₁ . b₁ = a₂ implies a₄ . b₁ = a₃ ) & ( a₁ . b₁ <> a₂ implies a₄ . b₁ = a₁ . b₁ ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines / ZF_LANG1:def 4 :

theorem Th165: :: ZF_LANG1:165

canceled;

theorem Th166: :: ZF_LANG1:166

for b₁, b₂, b₃, b₄, b₅, b₆ being Variable holds
( (b₁ '=' b₂) / b₃,b₄ = b₅ '=' b₆ iff ( ( b₁ <> b₃ & b₂ <> b₃ & b₅ = b₁ & b₆ = b₂ ) or ( b₁ = b₃ & b₂ <> b₃ & b₅ = b₄ & b₆ = b₂ ) or ( b₁ <> b₃ & b₂ = b₃ & b₅ = b₁ & b₆ = b₄ ) or ( b₁ = b₃ & b₂ = b₃ & b₅ = b₄ & b₆ = b₄ ) ) )

proof end;

theorem Th167: :: ZF_LANG1:167

for b₁, b₂, b₃, b₄ being Variable ex b₅, b₆ being Variable st (b₁ '=' b₂) / b₃,b₄ = b₅ '=' b₆

proof end;

theorem Th168: :: ZF_LANG1:168

for b₁, b₂, b₃, b₄, b₅, b₆ being Variable holds
( (b₁ 'in' b₂) / b₃,b₄ = b₅ 'in' b₆ iff ( ( b₁ <> b₃ & b₂ <> b₃ & b₅ = b₁ & b₆ = b₂ ) or ( b₁ = b₃ & b₂ <> b₃ & b₅ = b₄ & b₆ = b₂ ) or ( b₁ <> b₃ & b₂ = b₃ & b₅ = b₁ & b₆ = b₄ ) or ( b₁ = b₃ & b₂ = b₃ & b₅ = b₄ & b₆ = b₄ ) ) )

proof end;

theorem Th169: :: ZF_LANG1:169

for b₁, b₂, b₃, b₄ being Variable ex b₅, b₆ being Variable st (b₁ 'in' b₂) / b₃,b₄ = b₅ 'in' b₆

proof end;

theorem Th170: :: ZF_LANG1:170

for b₁, b₂ being ZF-formula
for b₃, b₄ being Variable holds
( 'not' b₁ = ('not' b₂) / b₃,b₄ iff b₁ = b₂ / b₃,b₄ )

proof end;

Lemma58: for b₁, b₂, b₃, b₄ being ZF-formula
for b₅, b₆ being Variable st b₁ = b₂ / b₅,b₆ & b₃ = b₄ / b₅,b₆ holds
b₁ '&' b₃ = (b₂ '&' b₄) / b₅,b₆

proof end;

Lemma59: for b₁, b₂ being ZF-formula
for b₃, b₄, b₅, b₆ being Variable st b₁ = b₂ / b₃,b₄ & ( ( b₅ = b₆ & b₆ <> b₃ ) or ( b₅ = b₄ & b₆ = b₃ ) ) holds
All b₅,b₁ = (All b₆,b₂) / b₃,b₄

proof end;

theorem Th171: :: ZF_LANG1:171

for b₁ being ZF-formula
for b₂, b₃ being Variable holds b₁ / b₂,b₃ in WFF

proof end;

definition

let c₁ be ZF-formula;
let c₂, c₃ be Variable;
redefine func / as c₁ / c₂,c₃ -> ZF-formula;
coherence

proof end;

end;

theorem Th172: :: ZF_LANG1:172

for b₁, b₂, b₃, b₄ being ZF-formula
for b₅, b₆ being Variable holds
( b₁ '&' b₂ = (b₃ '&' b₄) / b₅,b₆ iff ( b₁ = b₃ / b₅,b₆ & b₂ = b₄ / b₅,b₆ ) )

proof end;

theorem Th173: :: ZF_LANG1:173

for b₁, b₂ being ZF-formula
for b₃, b₄, b₅ being Variable st b₃ <> b₄ holds
( All b₃,b₁ = (All b₃,b₂) / b₄,b₅ iff b₁ = b₂ / b₄,b₅ )

proof end;

theorem Th174: :: ZF_LANG1:174

for b₁, b₂ being ZF-formula
for b₃, b₄ being Variable holds
( All b₃,b₁ = (All b₄,b₂) / b₄,b₃ iff b₁ = b₂ / b₄,b₃ )

proof end;

theorem Th175: :: ZF_LANG1:175

for b₁, b₂, b₃, b₄ being ZF-formula
for b₅, b₆ being Variable holds
( b₁ 'or' b₂ = (b₃ 'or' b₄) / b₅,b₆ iff ( b₁ = b₃ / b₅,b₆ & b₂ = b₄ / b₅,b₆ ) )

proof end;

theorem Th176: :: ZF_LANG1:176

for b₁, b₂, b₃, b₄ being ZF-formula
for b₅, b₆ being Variable holds
( b₁ => b₂ = (b₃ => b₄) / b₅,b₆ iff ( b₁ = b₃ / b₅,b₆ & b₂ = b₄ / b₅,b₆ ) )

proof end;

theorem Th177: :: ZF_LANG1:177

for b₁, b₂, b₃, b₄ being ZF-formula
for b₅, b₆ being Variable holds
( b₁ <=> b₂ = (b₃ <=> b₄) / b₅,b₆ iff ( b₁ = b₃ / b₅,b₆ & b₂ = b₄ / b₅,b₆ ) )

proof end;

theorem Th178: :: ZF_LANG1:178

for b₁, b₂ being ZF-formula
for b₃, b₄, b₅ being Variable st b₃ <> b₄ holds
( Ex b₃,b₁ = (Ex b₃,b₂) / b₄,b₅ iff b₁ = b₂ / b₄,b₅ )

proof end;

theorem Th179: :: ZF_LANG1:179

for b₁, b₂ being ZF-formula
for b₃, b₄ being Variable holds
( Ex b₃,b₁ = (Ex b₄,b₂) / b₄,b₃ iff b₁ = b₂ / b₄,b₃ )

proof end;

theorem Th180: :: ZF_LANG1:180

for b₁ being ZF-formula
for b₂, b₃ being Variable holds
( b₁ is_equality iff b₁ / b₂,b₃ is_equality )

proof end;

theorem Th181: :: ZF_LANG1:181

for b₁ being ZF-formula
for b₂, b₃ being Variable holds
( b₁ is_membership iff b₁ / b₂,b₃ is_membership )

proof end;

theorem Th182: :: ZF_LANG1:182

for b₁ being ZF-formula
for b₂, b₃ being Variable holds
( b₁ is negative iff b₁ / b₂,b₃ is negative )

proof end;

theorem Th183: :: ZF_LANG1:183

for b₁ being ZF-formula
for b₂, b₃ being Variable holds
( b₁ is conjunctive iff b₁ / b₂,b₃ is conjunctive )

proof end;

theorem Th184: :: ZF_LANG1:184

for b₁ being ZF-formula
for b₂, b₃ being Variable holds
( b₁ is universal iff b₁ / b₂,b₃ is universal )

proof end;

theorem Th185: :: ZF_LANG1:185

for b₁ being ZF-formula
for b₂, b₃ being Variable st b₁ is negative holds
the_argument_of (b₁ / b₂,b₃) = (the_argument_of b₁) / b₂,b₃

proof end;

theorem Th186: :: ZF_LANG1:186

for b₁ being ZF-formula
for b₂, b₃ being Variable st b₁ is conjunctive holds
( the_left_argument_of (b₁ / b₂,b₃) = (the_left_argument_of b₁) / b₂,b₃ & the_right_argument_of (b₁ / b₂,b₃) = (the_right_argument_of b₁) / b₂,b₃ )

proof end;

theorem Th187: :: ZF_LANG1:187

for b₁ being ZF-formula
for b₂, b₃ being Variable st b₁ is universal holds
( the_scope_of (b₁ / b₂,b₃) = (the_scope_of b₁) / b₂,b₃ & ( bound_in b₁ = b₂ implies bound_in (b₁ / b₂,b₃) = b₃ ) & ( bound_in b₁ <> b₂ implies bound_in (b₁ / b₂,b₃) = bound_in b₁ ) )

proof end;

theorem Th188: :: ZF_LANG1:188

for b₁ being ZF-formula
for b₂, b₃ being Variable holds
( b₁ is disjunctive iff b₁ / b₂,b₃ is disjunctive )

proof end;

theorem Th189: :: ZF_LANG1:189

for b₁ being ZF-formula
for b₂, b₃ being Variable holds
( b₁ is conditional iff b₁ / b₂,b₃ is conditional )

proof end;

theorem Th190: :: ZF_LANG1:190

for b₁ being ZF-formula
for b₂, b₃ being Variable st b₁ is biconditional holds
b₁ / b₂,b₃ is biconditional

proof end;

theorem Th191: :: ZF_LANG1:191

for b₁ being ZF-formula
for b₂, b₃ being Variable holds
( b₁ is existential iff b₁ / b₂,b₃ is existential )

proof end;

theorem Th192: :: ZF_LANG1:192

for b₁ being ZF-formula
for b₂, b₃ being Variable st b₁ is disjunctive holds
( the_left_argument_of (b₁ / b₂,b₃) = (the_left_argument_of b₁) / b₂,b₃ & the_right_argument_of (b₁ / b₂,b₃) = (the_right_argument_of b₁) / b₂,b₃ )

proof end;

theorem Th193: :: ZF_LANG1:193

for b₁ being ZF-formula
for b₂, b₃ being Variable st b₁ is conditional holds
( the_antecedent_of (b₁ / b₂,b₃) = (the_antecedent_of b₁) / b₂,b₃ & the_consequent_of (b₁ / b₂,b₃) = (the_consequent_of b₁) / b₂,b₃ )

proof end;

theorem Th194: :: ZF_LANG1:194

for b₁ being ZF-formula
for b₂, b₃ being Variable st b₁ is biconditional holds
( the_left_side_of (b₁ / b₂,b₃) = (the_left_side_of b₁) / b₂,b₃ & the_right_side_of (b₁ / b₂,b₃) = (the_right_side_of b₁) / b₂,b₃ )

proof end;

theorem Th195: :: ZF_LANG1:195

for b₁ being ZF-formula
for b₂, b₃ being Variable st b₁ is existential holds
( the_scope_of (b₁ / b₂,b₃) = (the_scope_of b₁) / b₂,b₃ & ( bound_in b₁ = b₂ implies bound_in (b₁ / b₂,b₃) = b₃ ) & ( bound_in b₁ <> b₂ implies bound_in (b₁ / b₂,b₃) = bound_in b₁ ) )

proof end;

theorem Th196: :: ZF_LANG1:196

for b₁ being ZF-formula
for b₂, b₃ being Variable st not b₂ in variables_in b₁ holds
b₁ / b₂,b₃ = b₁

proof end;

theorem Th197: :: ZF_LANG1:197

for b₁ being ZF-formula
for b₂ being Variable holds b₁ / b₂,b₂ = b₁

proof end;

theorem Th198: :: ZF_LANG1:198

for b₁ being ZF-formula
for b₂, b₃ being Variable st b₂ <> b₃ holds
not b₂ in variables_in (b₁ / b₂,b₃)

proof end;

theorem Th199: :: ZF_LANG1:199

for b₁ being ZF-formula
for b₂, b₃ being Variable st b₂ in variables_in b₁ holds
b₃ in variables_in (b₁ / b₂,b₃)

proof end;

theorem Th200: :: ZF_LANG1:200

for b₁ being ZF-formula
for b₂, b₃, b₄ being Variable st b₂ <> b₃ holds
(b₁ / b₂,b₃) / b₂,b₄ = b₁ / b₂,b₃

proof end;

theorem Th201: :: ZF_LANG1:201

for b₁ being ZF-formula
for b₂, b₃ being Variable holds variables_in (b₁ / b₂,b₃) c= ((variables_in b₁) \ {b₂}) \/ {b₃}

proof end;