:: ZF_LANG1 semantic presentation

begin


theorem Th1: :: ZF_LANG1:1
for x, y being Variable holds
( Var1 (x '=' y) = x & Var2 (x '=' y) = y )
proof
let x, y be Variable; ::_thesis: ( Var1 (x '=' y) = x & Var2 (x '=' y) = y )
 x '=' y is being_equality by ZF_LANG:5;
then  x '=' y = (Var1 (x '=' y)) '=' (Var2 (x '=' y)) by ZF_LANG:36;
hence  ( Var1 (x '=' y) = x & Var2 (x '=' y) = y ) by ZF_LANG:1; ::_thesis: verum
end;

theorem Th2: :: ZF_LANG1:2
for x, y being Variable holds
( Var1 (x 'in' y) = x & Var2 (x 'in' y) = y )
proof
let x, y be Variable; ::_thesis: ( Var1 (x 'in' y) = x & Var2 (x 'in' y) = y )
 x 'in' y is being_membership by ZF_LANG:5;
then  x 'in' y = (Var1 (x 'in' y)) 'in' (Var2 (x 'in' y)) by ZF_LANG:37;
hence  ( Var1 (x 'in' y) = x & Var2 (x 'in' y) = y ) by ZF_LANG:2; ::_thesis: verum
end;

theorem Th3: :: ZF_LANG1:3
for p being ZF-formula holds the_argument_of ('not' p) = p
proof
let p be ZF-formula; ::_thesis: the_argument_of ('not' p) = p
 'not' p is negative by ZF_LANG:5;
hence  the_argument_of ('not' p) = p by ZF_LANG:def_30; ::_thesis: verum
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
let p, q be ZF-formula; ::_thesis: ( the_left_argument_of (p '&' q) = p & the_right_argument_of (p '&' q) = q )
 p '&' q is conjunctive by ZF_LANG:5;
then  p '&' q = (the_left_argument_of (p '&' q)) '&' (the_right_argument_of (p '&' q)) by ZF_LANG:40;
hence  ( the_left_argument_of (p '&' q) = p & the_right_argument_of (p '&' q) = q ) by ZF_LANG:30; ::_thesis: verum
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
let p, q be ZF-formula; ::_thesis: ( the_left_argument_of (p 'or' q) = p & the_right_argument_of (p 'or' q) = q )
 p 'or' q is disjunctive by ZF_LANG:6;
then  p 'or' q = (the_left_argument_of (p 'or' q)) 'or' (the_right_argument_of (p 'or' q)) by ZF_LANG:41;
hence  ( the_left_argument_of (p 'or' q) = p & the_right_argument_of (p 'or' q) = q ) by ZF_LANG:31; ::_thesis: verum
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
let p, q be ZF-formula; ::_thesis: ( the_antecedent_of (p => q) = p & the_consequent_of (p => q) = q )
 p => q is conditional by ZF_LANG:6;
then  p => q = (the_antecedent_of (p => q)) => (the_consequent_of (p => q)) by ZF_LANG:47;
hence  ( the_antecedent_of (p => q) = p & the_consequent_of (p => q) = q ) by ZF_LANG:32; ::_thesis: verum
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
let p, q be ZF-formula; ::_thesis: ( the_left_side_of (p <=> q) = p & the_right_side_of (p <=> q) = q )
 p <=> q is biconditional by ZF_LANG:6;
then  p <=> q = (the_left_side_of (p <=> q)) <=> (the_right_side_of (p <=> q)) by ZF_LANG:49;
hence  ( the_left_side_of (p <=> q) = p & the_right_side_of (p <=> q) = q ) by ZF_LANG:33; ::_thesis: verum
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
let p be ZF-formula; ::_thesis: for x being Variable holds
( bound_in (All (x,p)) = x & the_scope_of (All (x,p)) = p )
let x be Variable; ::_thesis: ( bound_in (All (x,p)) = x & the_scope_of (All (x,p)) = p )
 All (x,p) is universal by ZF_LANG:5;
then  All (x,p) = All ((bound_in (All (x,p))),(the_scope_of (All (x,p)))) by ZF_LANG:44;
hence  ( bound_in (All (x,p)) = x & the_scope_of (All (x,p)) = p ) by ZF_LANG:3; ::_thesis: verum
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
let p be ZF-formula; ::_thesis: for x being Variable holds
( bound_in (Ex (x,p)) = x & the_scope_of (Ex (x,p)) = p )
let x be Variable; ::_thesis: ( bound_in (Ex (x,p)) = x & the_scope_of (Ex (x,p)) = p )
 Ex (x,p) is existential by ZF_LANG:6;
then  Ex (x,p) = Ex ((bound_in (Ex (x,p))),(the_scope_of (Ex (x,p)))) by ZF_LANG:45;
hence  ( bound_in (Ex (x,p)) = x & the_scope_of (Ex (x,p)) = p ) by ZF_LANG:34; ::_thesis: verum
end;

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

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

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;

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

theorem Th14: :: ZF_LANG1:14
for p1, p2 being ZF-formula
for x1, y1, x2, y2 being Variable st All (x1,y1,p1) = All (x2,y2,p2) holds
( x1 = x2 & y1 = y2 & p1 = p2 )
proof
let p1, p2 be ZF-formula; ::_thesis: for x1, y1, x2, y2 being Variable st All (x1,y1,p1) = All (x2,y2,p2) holds
( x1 = x2 & y1 = y2 & p1 = p2 )
let x1, y1, x2, y2 be Variable; ::_thesis: ( All (x1,y1,p1) = All (x2,y2,p2) implies ( x1 = x2 & y1 = y2 & p1 = p2 ) )
assume A1: All (x1,y1,p1) = All (x2,y2,p2) ; ::_thesis: ( x1 = x2 & y1 = y2 & p1 = p2 )
then  All (y1,p1) = All (y2,p2) by ZF_LANG:3;
hence  ( x1 = x2 & y1 = y2 & p1 = p2 ) by A1, ZF_LANG:3; ::_thesis: verum
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 )
proof
let p1, p2 be ZF-formula; ::_thesis: 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 )
let x1, y1, z1, x2, y2, z2 be Variable; ::_thesis: ( All (x1,y1,z1,p1) = All (x2,y2,z2,p2) implies ( x1 = x2 & y1 = y2 & z1 = z2 & p1 = p2 ) )
assume A1: All (x1,y1,z1,p1) = All (x2,y2,z2,p2) ; ::_thesis: ( x1 = x2 & y1 = y2 & z1 = z2 & p1 = p2 )
then  All (y1,z1,p1) = All (y2,z2,p2) by ZF_LANG:3;
hence  ( x1 = x2 & y1 = y2 & z1 = z2 & p1 = p2 ) by A1, Th14, ZF_LANG:3; ::_thesis: verum
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 )
proof
let p, q be ZF-formula; ::_thesis: 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 )
let x, y, z, t, s be Variable; ::_thesis: ( All (x,y,z,p) = All (t,s,q) implies ( x = t & y = s & All (z,p) = q ) )
 All (x,y,z,p) = All (x,y,(All (z,p))) ;
hence  ( All (x,y,z,p) = All (t,s,q) implies ( x = t & y = s & All (z,p) = q ) ) by Th14; ::_thesis: verum
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 )
proof
let p1, p2 be ZF-formula; ::_thesis: for x1, y1, x2, y2 being Variable st Ex (x1,y1,p1) = Ex (x2,y2,p2) holds
( x1 = x2 & y1 = y2 & p1 = p2 )
let x1, y1, x2, y2 be Variable; ::_thesis: ( Ex (x1,y1,p1) = Ex (x2,y2,p2) implies ( x1 = x2 & y1 = y2 & p1 = p2 ) )
assume A1: Ex (x1,y1,p1) = Ex (x2,y2,p2) ; ::_thesis: ( x1 = x2 & y1 = y2 & p1 = p2 )
then  Ex (y1,p1) = Ex (y2,p2) by ZF_LANG:34;
hence  ( x1 = x2 & y1 = y2 & p1 = p2 ) by A1, ZF_LANG:34; ::_thesis: verum
end;

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

theorem :: ZF_LANG1:19
for p1, p2 being ZF-formula
for x1, 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
let p1, p2 be ZF-formula; ::_thesis: 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 )
let x1, y1, z1, x2, y2, z2 be Variable; ::_thesis: ( Ex (x1,y1,z1,p1) = Ex (x2,y2,z2,p2) implies ( x1 = x2 & y1 = y2 & z1 = z2 & p1 = p2 ) )
assume A1: Ex (x1,y1,z1,p1) = Ex (x2,y2,z2,p2) ; ::_thesis: ( x1 = x2 & y1 = y2 & z1 = z2 & p1 = p2 )
then  Ex (y1,z1,p1) = Ex (y2,z2,p2) by ZF_LANG:34;
hence  ( x1 = x2 & y1 = y2 & z1 = z2 & p1 = p2 ) by A1, Th17, ZF_LANG:34; ::_thesis: verum
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 )
proof
let p, q be ZF-formula; ::_thesis: 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 )
let x, y, z, t, s be Variable; ::_thesis: ( Ex (x,y,z,p) = Ex (t,s,q) implies ( x = t & y = s & Ex (z,p) = q ) )
 Ex (x,y,z,p) = Ex (x,y,(Ex (z,p))) ;
hence  ( Ex (x,y,z,p) = Ex (t,s,q) implies ( x = t & y = s & Ex (z,p) = q ) ) by Th17; ::_thesis: verum
end;

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

theorem :: ZF_LANG1:22
for p being ZF-formula
for x, y, z being Variable holds
( Ex (x,y,z,p) is existential & 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))
proof
let H be ZF-formula; ::_thesis: ( H is disjunctive implies the_left_argument_of H = the_argument_of (the_left_argument_of (the_argument_of H)) )
assume  H is disjunctive ; ::_thesis: the_left_argument_of H = the_argument_of (the_left_argument_of (the_argument_of H))
then  H = (the_left_argument_of H) 'or' (the_right_argument_of H) by ZF_LANG:41;
then  the_argument_of H = ('not' (the_left_argument_of H)) '&' ('not' (the_right_argument_of H)) by Th3;
then  the_left_argument_of (the_argument_of H) = 'not' (the_left_argument_of H) by Th4;
hence  the_left_argument_of H = the_argument_of (the_left_argument_of (the_argument_of H)) by Th3; ::_thesis: verum
end;

theorem :: ZF_LANG1:24
for H being ZF-formula st H is disjunctive holds
the_right_argument_of H = the_argument_of (the_right_argument_of (the_argument_of H))
proof
let H be ZF-formula; ::_thesis: ( H is disjunctive implies the_right_argument_of H = the_argument_of (the_right_argument_of (the_argument_of H)) )
assume  H is disjunctive ; ::_thesis: the_right_argument_of H = the_argument_of (the_right_argument_of (the_argument_of H))
then  H = (the_left_argument_of H) 'or' (the_right_argument_of H) by ZF_LANG:41;
then  the_argument_of H = ('not' (the_left_argument_of H)) '&' ('not' (the_right_argument_of H)) by Th3;
then  the_right_argument_of (the_argument_of H) = 'not' (the_right_argument_of H) by Th4;
hence  the_right_argument_of H = the_argument_of (the_right_argument_of (the_argument_of H)) by Th3; ::_thesis: verum
end;

theorem :: ZF_LANG1:25
for H being ZF-formula st H is conditional holds
the_antecedent_of H = the_left_argument_of (the_argument_of H)
proof
let H be ZF-formula; ::_thesis: ( H is conditional implies the_antecedent_of H = the_left_argument_of (the_argument_of H) )
assume  H is conditional ; ::_thesis: the_antecedent_of H = the_left_argument_of (the_argument_of H)
then  H = (the_antecedent_of H) => (the_consequent_of H) by ZF_LANG:47;
then  the_argument_of H = (the_antecedent_of H) '&' ('not' (the_consequent_of H)) by Th3;
hence  the_antecedent_of H = the_left_argument_of (the_argument_of H) by Th4; ::_thesis: verum
end;

theorem :: ZF_LANG1:26
for H being ZF-formula st H is conditional holds
the_consequent_of H = the_argument_of (the_right_argument_of (the_argument_of H))
proof
let H be ZF-formula; ::_thesis: ( H is conditional implies the_consequent_of H = the_argument_of (the_right_argument_of (the_argument_of H)) )
assume  H is conditional ; ::_thesis: the_consequent_of H = the_argument_of (the_right_argument_of (the_argument_of H))
then  H = (the_antecedent_of H) => (the_consequent_of H) by ZF_LANG:47;
then  the_argument_of H = (the_antecedent_of H) '&' ('not' (the_consequent_of H)) by Th3;
then  the_right_argument_of (the_argument_of H) = 'not' (the_consequent_of H) by Th4;
hence  the_consequent_of H = the_argument_of (the_right_argument_of (the_argument_of H)) by Th3; ::_thesis: verum
end;

theorem :: ZF_LANG1:27
for H being ZF-formula st H is biconditional holds
( the_left_side_of H = the_antecedent_of (the_left_argument_of H) & the_left_side_of H = the_consequent_of (the_right_argument_of H) )
proof
let H be ZF-formula; ::_thesis: ( H is biconditional implies ( 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) ) )
assume  H is biconditional ; ::_thesis: ( 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) )
then  H = (the_left_side_of H) <=> (the_right_side_of H) by ZF_LANG:49;
then  ( the_left_argument_of H = (the_left_side_of H) => (the_right_side_of H) & the_right_argument_of H = (the_right_side_of H) => (the_left_side_of H) ) by Th4;
hence  ( 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) ) by Th6; ::_thesis: verum
end;

theorem :: ZF_LANG1:28
for H being ZF-formula st H is biconditional holds
( the_right_side_of H = the_consequent_of (the_left_argument_of H) & the_right_side_of H = the_antecedent_of (the_right_argument_of H) )
proof
let H be ZF-formula; ::_thesis: ( H is biconditional implies ( 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) ) )
assume  H is biconditional ; ::_thesis: ( 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) )
then  H = (the_left_side_of H) <=> (the_right_side_of H) by ZF_LANG:49;
then  ( the_left_argument_of H = (the_left_side_of H) => (the_right_side_of H) & the_right_argument_of H = (the_right_side_of H) => (the_left_side_of H) ) by Th4;
hence  ( 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) ) by Th6; ::_thesis: verum
end;

theorem :: ZF_LANG1:29
for H being ZF-formula st H is existential holds
( bound_in H = bound_in (the_argument_of H) & the_scope_of H = the_argument_of (the_scope_of (the_argument_of H)) )
proof
let H be ZF-formula; ::_thesis: ( H is existential implies ( bound_in H = bound_in (the_argument_of H) & the_scope_of H = the_argument_of (the_scope_of (the_argument_of H)) ) )
assume  H is existential ; ::_thesis: ( bound_in H = bound_in (the_argument_of H) & the_scope_of H = the_argument_of (the_scope_of (the_argument_of H)) )
then  H = Ex ((bound_in H),(the_scope_of H)) by ZF_LANG:45;
then A1: the_argument_of H = All ((bound_in H),('not' (the_scope_of H))) by Th3;
hence  bound_in H = bound_in (the_argument_of H) by Th8; ::_thesis: the_scope_of H = the_argument_of (the_scope_of (the_argument_of H))
 'not' (the_scope_of H) = the_scope_of (the_argument_of H) by A1, Th8;
hence  the_scope_of H = the_argument_of (the_scope_of (the_argument_of H)) by Th3; ::_thesis: verum
end;

theorem :: ZF_LANG1:30
for F, G being ZF-formula holds
( the_argument_of (F 'or' G) = ('not' F) '&' ('not' G) & the_antecedent_of (F 'or' G) = 'not' F & the_consequent_of (F 'or' G) = G )
proof
let F, G be ZF-formula; ::_thesis: ( 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 )
thus  the_argument_of (F 'or' G) = ('not' F) '&' ('not' G) by Th3; ::_thesis: ( the_antecedent_of (F 'or' G) = 'not' F & the_consequent_of (F 'or' G) = G )
 F 'or' G = ('not' F) => G ;
hence  ( the_antecedent_of (F 'or' G) = 'not' F & the_consequent_of (F 'or' G) = G ) by Th6; ::_thesis: verum
end;

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

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

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

theorem :: ZF_LANG1:34
for H being ZF-formula st H is disjunctive holds
( H is conditional & H is negative & the_argument_of H is conjunctive & the_left_argument_of (the_argument_of H) is negative & the_right_argument_of (the_argument_of H) is negative )
proof
let H be ZF-formula; ::_thesis: ( H is disjunctive implies ( 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 ) )
assume  H is disjunctive ; ::_thesis: ( 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 )
then A1: H = (the_left_argument_of H) 'or' (the_right_argument_of H) by ZF_LANG:41;
then  H = ('not' (the_left_argument_of H)) => (the_right_argument_of H) ;
hence  ( H is conditional & H is negative ) by ZF_LANG:5, ZF_LANG:6; ::_thesis: ( 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 )
A2: the_argument_of H = ('not' (the_left_argument_of H)) '&' ('not' (the_right_argument_of H)) by A1, Th3;
hence  the_argument_of H is conjunctive by ZF_LANG:5; ::_thesis: ( the_left_argument_of (the_argument_of H) is negative & the_right_argument_of (the_argument_of H) is negative )
 ( the_left_argument_of (the_argument_of H) = 'not' (the_left_argument_of H) & the_right_argument_of (the_argument_of H) = 'not' (the_right_argument_of H) ) by A2, Th4;
hence  ( the_left_argument_of (the_argument_of H) is negative & the_right_argument_of (the_argument_of H) is negative ) by ZF_LANG:5; ::_thesis: verum
end;

theorem :: ZF_LANG1:35
for H being ZF-formula st H is conditional holds
( H is negative & the_argument_of H is conjunctive & the_right_argument_of (the_argument_of H) is negative )
proof
let H be ZF-formula; ::_thesis: ( H is conditional implies ( H is negative & the_argument_of H is conjunctive & the_right_argument_of (the_argument_of H) is negative ) )
assume  H is conditional ; ::_thesis: ( H is negative & the_argument_of H is conjunctive & the_right_argument_of (the_argument_of H) is negative )
then A1: H = (the_antecedent_of H) => (the_consequent_of H) by ZF_LANG:47;
hence  H is negative by ZF_LANG:5; ::_thesis: ( the_argument_of H is conjunctive & the_right_argument_of (the_argument_of H) is negative )
A2: the_argument_of H = (the_antecedent_of H) '&' ('not' (the_consequent_of H)) by A1, Th3;
hence  the_argument_of H is conjunctive by ZF_LANG:5; ::_thesis: the_right_argument_of (the_argument_of H) is negative
 the_right_argument_of (the_argument_of H) = 'not' (the_consequent_of H) by A2, Th4;
hence  the_right_argument_of (the_argument_of H) is negative by ZF_LANG:5; ::_thesis: verum
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 )
proof
let H be ZF-formula; ::_thesis: ( H is biconditional implies ( H is conjunctive & the_left_argument_of H is conditional & the_right_argument_of H is conditional ) )
assume  H is biconditional ; ::_thesis: ( H is conjunctive & the_left_argument_of H is conditional & the_right_argument_of H is conditional )
then A1: H = (the_left_side_of H) <=> (the_right_side_of H) by ZF_LANG:49;
hence  H is conjunctive by ZF_LANG:5; ::_thesis: ( the_left_argument_of H is conditional & the_right_argument_of H is conditional )
 ( the_left_argument_of H = (the_left_side_of H) => (the_right_side_of H) & the_right_argument_of H = (the_right_side_of H) => (the_left_side_of H) ) by A1, Th4;
hence  ( the_left_argument_of H is conditional & the_right_argument_of H is conditional ) by ZF_LANG:6; ::_thesis: verum
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 )
proof
let H be ZF-formula; ::_thesis: ( H is existential implies ( H is negative & the_argument_of H is universal & the_scope_of (the_argument_of H) is negative ) )
assume  H is existential ; ::_thesis: ( H is negative & the_argument_of H is universal & the_scope_of (the_argument_of H) is negative )
then A1: H = Ex ((bound_in H),(the_scope_of H)) by ZF_LANG:45;
hence  H is negative by ZF_LANG:5; ::_thesis: ( the_argument_of H is universal & the_scope_of (the_argument_of H) is negative )
A2: the_argument_of H = All ((bound_in H),('not' (the_scope_of H))) by A1, Th3;
hence  the_argument_of H is universal by ZF_LANG:5; ::_thesis: the_scope_of (the_argument_of H) is negative
 'not' (the_scope_of H) = the_scope_of (the_argument_of H) by A2, Th8;
hence  the_scope_of (the_argument_of H) is negative by ZF_LANG:5; ::_thesis: verum
end;

theorem :: ZF_LANG1:38
for H being ZF-formula holds
( ( not H is being_equality or ( not H is being_membership & not H is negative & not H is conjunctive & not H is universal ) ) & ( not H is being_membership or ( not H is negative & not H is conjunctive & not H is universal ) ) & ( not H is negative or ( not H is conjunctive & not H is universal ) ) & ( not H is conjunctive or not H is universal ) )
proof
let H be ZF-formula; ::_thesis: ( ( 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 ) )
 ( H . 1 = 0 or H . 1 = 1 or H . 1 = 2 or H . 1 = 3 or H . 1 = 4 ) by ZF_LANG:23;
hence  ( ( 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 ) ) by ZF_LANG:18, ZF_LANG:19, ZF_LANG:20, ZF_LANG:21, ZF_LANG:22; ::_thesis: verum
end;

theorem Th39: :: ZF_LANG1:39
for F, G being ZF-formula st F is_subformula_of G holds
len F <= len G
proof
let F, G be ZF-formula; ::_thesis: ( F is_subformula_of G implies len F <= len G )
assume  F is_subformula_of G ; ::_thesis: len F <= len G
then  ( F is_proper_subformula_of G or F = G ) by ZF_LANG:def_41;
hence  len F <= len G by ZF_LANG:62; ::_thesis: verum
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
proof
let F, G, H be ZF-formula; ::_thesis: ( ( ( 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 ) ) implies F is_proper_subformula_of H )
A1: ( F is_immediate_constituent_of G implies F is_proper_subformula_of G ) by ZF_LANG:61;
A2: now__::_thesis:_(_F_is_proper_subformula_of_G_&_G_is_subformula_of_H_implies_F_is_proper_subformula_of_H_)
assume A3: F is_proper_subformula_of G ; ::_thesis: ( G is_subformula_of H implies F is_proper_subformula_of H )
then A4: len F < len G by ZF_LANG:62;
assume A5: G is_subformula_of H ; ::_thesis: F is_proper_subformula_of H
 F is_subformula_of G by A3, ZF_LANG:def_41;
then A6: F is_subformula_of H by A5, ZF_LANG:65;
 len G <= len H by A5, Th39;
hence  F is_proper_subformula_of H by A4, A6, ZF_LANG:def_41; ::_thesis: verum
end;
A7: now__::_thesis:_(_F_is_subformula_of_G_&_G_is_proper_subformula_of_H_&_(_(_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_)_)_implies_F_is_proper_subformula_of_H_)
assume that
A8: F is_subformula_of G and
A9: G is_proper_subformula_of H ; ::_thesis: ( ( ( 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 ) ) implies F is_proper_subformula_of H )
 G is_subformula_of H by A9, ZF_LANG:def_41;
then A10: F is_subformula_of H by A8, ZF_LANG:65;
 len F <= len G by A8, Th39;
then  len F < len H by A9, XXREAL_0:2, ZF_LANG:62;
hence  ( ( ( 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 ) ) implies F is_proper_subformula_of H ) by A10, ZF_LANG:def_41; ::_thesis: verum
end;
 ( G is_immediate_constituent_of H implies G is_proper_subformula_of H ) by ZF_LANG:61;
hence  ( ( ( 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 ) ) implies F is_proper_subformula_of H ) by A2, A7, A1, ZF_LANG:64; ::_thesis: verum
end;

theorem :: ZF_LANG1:41
for H being ZF-formula holds not H is_immediate_constituent_of H
proof
let H be ZF-formula; ::_thesis: not H is_immediate_constituent_of H
assume  H is_immediate_constituent_of H ; ::_thesis: contradiction
then  H is_proper_subformula_of H by ZF_LANG:61;
hence  contradiction by ZF_LANG:def_41; ::_thesis: verum
end;

theorem :: ZF_LANG1:42
for G, H being ZF-formula holds
( not G is_proper_subformula_of H or not H is_subformula_of G )
proof
let G, H be ZF-formula; ::_thesis: ( not G is_proper_subformula_of H or not H is_subformula_of G )
assume  ( G is_proper_subformula_of H & H is_subformula_of G ) ; ::_thesis: contradiction
then  G is_proper_subformula_of G by Th40;
hence  contradiction by ZF_LANG:def_41; ::_thesis: verum
end;

theorem :: ZF_LANG1:43
for G, H being ZF-formula holds
( not G is_proper_subformula_of H or not H is_proper_subformula_of G )
proof
let G, H be ZF-formula; ::_thesis: ( not G is_proper_subformula_of H or not H is_proper_subformula_of G )
assume  ( G is_proper_subformula_of H & H is_proper_subformula_of G ) ; ::_thesis: contradiction
then  G is_proper_subformula_of G by ZF_LANG:64;
hence  contradiction by ZF_LANG:def_41; ::_thesis: verum
end;

theorem :: ZF_LANG1:44
for G, H being ZF-formula holds
( not G is_subformula_of H or not H is_immediate_constituent_of G )
proof
let G, H be ZF-formula; ::_thesis: ( not G is_subformula_of H or not H is_immediate_constituent_of G )
assume  ( G is_subformula_of H & H is_immediate_constituent_of G ) ; ::_thesis: contradiction
then  G is_proper_subformula_of G by Th40;
hence  contradiction by ZF_LANG:def_41; ::_thesis: verum
end;

theorem :: ZF_LANG1:45
for G, H being ZF-formula holds
( not G is_proper_subformula_of H or not H is_immediate_constituent_of G )
proof
let G, H be ZF-formula; ::_thesis: ( not G is_proper_subformula_of H or not H is_immediate_constituent_of G )
assume  ( G is_proper_subformula_of H & H is_immediate_constituent_of G ) ; ::_thesis: contradiction
then  G is_proper_subformula_of G by Th40;
hence  contradiction by ZF_LANG:def_41; ::_thesis: verum
end;

theorem :: ZF_LANG1:46
for F, H being ZF-formula st 'not' F is_subformula_of H holds
F is_proper_subformula_of H
proof
let F, H be ZF-formula; ::_thesis: ( 'not' F is_subformula_of H implies F is_proper_subformula_of H )
 F is_immediate_constituent_of 'not' F by ZF_LANG:def_39;
hence  ( 'not' F is_subformula_of H implies F is_proper_subformula_of H ) by Th40; ::_thesis: verum
end;

theorem :: ZF_LANG1:47
for F, G, H being ZF-formula st F '&' G is_subformula_of H holds
( F is_proper_subformula_of H & G is_proper_subformula_of H )
proof
let F, G, H be ZF-formula; ::_thesis: ( F '&' G is_subformula_of H implies ( F is_proper_subformula_of H & G is_proper_subformula_of H ) )
 ( F is_immediate_constituent_of F '&' G & G is_immediate_constituent_of F '&' G ) by ZF_LANG:def_39;
hence  ( F '&' G is_subformula_of H implies ( F is_proper_subformula_of H & G is_proper_subformula_of H ) ) by Th40; ::_thesis: verum
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
proof
let H, F be ZF-formula; ::_thesis: for x being Variable st All (x,H) is_subformula_of F holds
H is_proper_subformula_of F
let x be Variable; ::_thesis: ( All (x,H) is_subformula_of F implies H is_proper_subformula_of F )
 H is_immediate_constituent_of All (x,H) by ZF_LANG:def_39;
hence  ( All (x,H) is_subformula_of F implies H is_proper_subformula_of F ) by Th40; ::_thesis: verum
end;

theorem :: ZF_LANG1:49
for F, G being ZF-formula holds
( F '&' ('not' G) is_proper_subformula_of F => G & F is_proper_subformula_of F => G & 'not' G is_proper_subformula_of F => G & G is_proper_subformula_of F => G )
proof
let F, G be ZF-formula; ::_thesis: ( 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_immediate_constituent_of F => G by ZF_LANG:def_39;
hence A1: F '&' ('not' G) is_proper_subformula_of F => G by ZF_LANG:61; ::_thesis: ( F is_proper_subformula_of F => G & 'not' G is_proper_subformula_of F => G & G is_proper_subformula_of F => G )
 ( F is_immediate_constituent_of F '&' ('not' G) & 'not' G is_immediate_constituent_of F '&' ('not' G) ) by ZF_LANG:def_39;
hence A2: ( F is_proper_subformula_of F => G & 'not' G is_proper_subformula_of F => G ) by A1, Th40; ::_thesis: G is_proper_subformula_of F => G
 G is_immediate_constituent_of 'not' G by ZF_LANG:def_39;
hence  G is_proper_subformula_of F => G by A2, Th40; ::_thesis: verum
end;

theorem :: ZF_LANG1:50
for F, G being ZF-formula holds
( ('not' F) '&' ('not' G) is_proper_subformula_of F 'or' G & 'not' F is_proper_subformula_of F 'or' G & 'not' G is_proper_subformula_of F 'or' G & F is_proper_subformula_of F 'or' G & G is_proper_subformula_of F 'or' G )
proof
let F, G be ZF-formula; ::_thesis: ( ('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_immediate_constituent_of F 'or' G by ZF_LANG:def_39;
hence A1: ('not' F) '&' ('not' G) is_proper_subformula_of F 'or' G by ZF_LANG:61; ::_thesis: ( '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 is_immediate_constituent_of ('not' F) '&' ('not' G) & 'not' G is_immediate_constituent_of ('not' F) '&' ('not' G) ) by ZF_LANG:def_39;
hence A2: ( 'not' F is_proper_subformula_of F 'or' G & 'not' G is_proper_subformula_of F 'or' G ) by A1, Th40; ::_thesis: ( F is_proper_subformula_of F 'or' G & G is_proper_subformula_of F 'or' G )
 ( F is_immediate_constituent_of 'not' F & G is_immediate_constituent_of 'not' G ) by ZF_LANG:def_39;
hence  ( F is_proper_subformula_of F 'or' G & G is_proper_subformula_of F 'or' G ) by A2, Th40; ::_thesis: verum
end;

theorem :: ZF_LANG1:51
for H being ZF-formula
for x being Variable holds
( All (x,('not' H)) is_proper_subformula_of Ex (x,H) & 'not' H is_proper_subformula_of Ex (x,H) )
proof
let H be ZF-formula; ::_thesis: 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) )
let x be Variable; ::_thesis: ( All (x,('not' H)) is_proper_subformula_of Ex (x,H) & 'not' H is_proper_subformula_of Ex (x,H) )
 All (x,('not' H)) is_immediate_constituent_of Ex (x,H) by ZF_LANG:def_39;
hence A1: All (x,('not' H)) is_proper_subformula_of Ex (x,H) by ZF_LANG:61; ::_thesis: 'not' H is_proper_subformula_of Ex (x,H)
 'not' H is_immediate_constituent_of All (x,('not' H)) by ZF_LANG:def_39;
hence  'not' H is_proper_subformula_of Ex (x,H) by A1, Th40; ::_thesis: verum
end;

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

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

theorem :: ZF_LANG1:54
for H being ZF-formula holds H in Subformulae H
proof
let H be ZF-formula; ::_thesis: H in Subformulae H
 H is_subformula_of H by ZF_LANG:59;
hence  H in Subformulae H by ZF_LANG:def_42; ::_thesis: verum
end;

theorem Th55: :: ZF_LANG1:55
for F, G being ZF-formula holds Subformulae (F => G) = ((Subformulae F) \/ (Subformulae G)) \/ {('not' G),(F '&' ('not' G)),(F => G)}
proof
let F, G be ZF-formula; ::_thesis: Subformulae (F => G) = ((Subformulae F) \/ (Subformulae G)) \/ {('not' G),(F '&' ('not' G)),(F => G)}
thus  Subformulae (F => G) = (Subformulae (F '&' ('not' G))) \/ {(F => G)} by ZF_LANG:82
.= (((Subformulae F) \/ (Subformulae ('not' G))) \/ {(F '&' ('not' G))}) \/ {(F => G)} by ZF_LANG:83
.= (((Subformulae F) \/ ((Subformulae G) \/ {('not' G)})) \/ {(F '&' ('not' G))}) \/ {(F => G)} by ZF_LANG:82
.= ((((Subformulae F) \/ (Subformulae G)) \/ {('not' G)}) \/ {(F '&' ('not' G))}) \/ {(F => G)} by XBOOLE_1:4
.= (((Subformulae F) \/ (Subformulae G)) \/ {('not' G)}) \/ ({(F '&' ('not' G))} \/ {(F => G)}) by XBOOLE_1:4
.= ((Subformulae F) \/ (Subformulae G)) \/ ({('not' G)} \/ ({(F '&' ('not' G))} \/ {(F => G)})) by XBOOLE_1:4
.= ((Subformulae F) \/ (Subformulae G)) \/ ({('not' G)} \/ {(F '&' ('not' G)),(F => G)}) by ENUMSET1:1
.= ((Subformulae F) \/ (Subformulae G)) \/ {('not' G),(F '&' ('not' G)),(F => G)} by ENUMSET1:2 ; ::_thesis: verum
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
let F, G be ZF-formula; ::_thesis: Subformulae (F 'or' G) = ((Subformulae F) \/ (Subformulae G)) \/ {('not' G),('not' F),(('not' F) '&' ('not' G)),(F 'or' G)}
thus  Subformulae (F 'or' G) = (Subformulae (('not' F) '&' ('not' G))) \/ {(F 'or' G)} by ZF_LANG:82
.= (((Subformulae ('not' F)) \/ (Subformulae ('not' G))) \/ {(('not' F) '&' ('not' G))}) \/ {(F 'or' G)} by ZF_LANG:83
.= (((Subformulae ('not' F)) \/ ((Subformulae G) \/ {('not' G)})) \/ {(('not' F) '&' ('not' G))}) \/ {(F 'or' G)} by ZF_LANG:82
.= ((((Subformulae F) \/ {('not' F)}) \/ ((Subformulae G) \/ {('not' G)})) \/ {(('not' F) '&' ('not' G))}) \/ {(F 'or' G)} by ZF_LANG:82
.= (((Subformulae F) \/ (((Subformulae G) \/ {('not' G)}) \/ {('not' F)})) \/ {(('not' F) '&' ('not' G))}) \/ {(F 'or' G)} by XBOOLE_1:4
.= (((Subformulae F) \/ ((Subformulae G) \/ ({('not' G)} \/ {('not' F)}))) \/ {(('not' F) '&' ('not' G))}) \/ {(F 'or' G)} by XBOOLE_1:4
.= (((Subformulae F) \/ ((Subformulae G) \/ {('not' G),('not' F)})) \/ {(('not' F) '&' ('not' G))}) \/ {(F 'or' G)} by ENUMSET1:1
.= ((((Subformulae F) \/ (Subformulae G)) \/ {('not' G),('not' F)}) \/ {(('not' F) '&' ('not' G))}) \/ {(F 'or' G)} by XBOOLE_1:4
.= (((Subformulae F) \/ (Subformulae G)) \/ {('not' G),('not' F)}) \/ ({(('not' F) '&' ('not' G))} \/ {(F 'or' G)}) by XBOOLE_1:4
.= (((Subformulae F) \/ (Subformulae G)) \/ {('not' G),('not' F)}) \/ {(('not' F) '&' ('not' G)),(F 'or' G)} by ENUMSET1:1
.= ((Subformulae F) \/ (Subformulae G)) \/ ({('not' G),('not' F)} \/ {(('not' F) '&' ('not' G)),(F 'or' G)}) by XBOOLE_1:4
.= ((Subformulae F) \/ (Subformulae G)) \/ {('not' G),('not' F),(('not' F) '&' ('not' G)),(F 'or' G)} by ENUMSET1:5 ; ::_thesis: verum
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
let F, G be ZF-formula; ::_thesis: Subformulae (F <=> G) = ((Subformulae F) \/ (Subformulae G)) \/ {('not' G),(F '&' ('not' G)),(F => G),('not' F),(G '&' ('not' F)),(G => F),(F <=> G)}
thus  Subformulae (F <=> G) = ((Subformulae (F => G)) \/ (Subformulae (G => F))) \/ {(F <=> G)} by ZF_LANG:83
.= ((((Subformulae F) \/ (Subformulae G)) \/ {('not' G),(F '&' ('not' G)),(F => G)}) \/ (Subformulae (G => F))) \/ {(F <=> G)} by Th55
.= ((((Subformulae F) \/ (Subformulae G)) \/ {('not' G),(F '&' ('not' G)),(F => G)}) \/ (((Subformulae F) \/ (Subformulae G)) \/ {('not' F),(G '&' ('not' F)),(G => F)})) \/ {(F <=> G)} by Th55
.= (((Subformulae F) \/ (Subformulae G)) \/ ((((Subformulae F) \/ (Subformulae G)) \/ {('not' G),(F '&' ('not' G)),(F => G)}) \/ {('not' F),(G '&' ('not' F)),(G => F)})) \/ {(F <=> G)} by XBOOLE_1:4
.= (((Subformulae F) \/ (Subformulae G)) \/ (((Subformulae F) \/ (Subformulae G)) \/ ({('not' G),(F '&' ('not' G)),(F => G)} \/ {('not' F),(G '&' ('not' F)),(G => F)}))) \/ {(F <=> G)} by XBOOLE_1:4
.= ((((Subformulae F) \/ (Subformulae G)) \/ ((Subformulae F) \/ (Subformulae G))) \/ ({('not' G),(F '&' ('not' G)),(F => G)} \/ {('not' F),(G '&' ('not' F)),(G => F)})) \/ {(F <=> G)} by XBOOLE_1:4
.= (((Subformulae F) \/ (Subformulae G)) \/ {('not' G),(F '&' ('not' G)),(F => G),('not' F),(G '&' ('not' F)),(G => F)}) \/ {(F <=> G)} by ENUMSET1:13
.= ((Subformulae F) \/ (Subformulae G)) \/ ({('not' G),(F '&' ('not' G)),(F => G),('not' F),(G '&' ('not' F)),(G => F)} \/ {(F <=> G)}) by XBOOLE_1:4
.= ((Subformulae F) \/ (Subformulae G)) \/ {('not' G),(F '&' ('not' G)),(F => G),('not' F),(G '&' ('not' F)),(G => F),(F <=> G)} by ENUMSET1:21 ; ::_thesis: verum
end;

theorem Th58: :: ZF_LANG1:58
for x, y being Variable holds Free (x '=' y) = {x,y}
proof
let x, y be Variable; ::_thesis: Free (x '=' y) = {x,y}
A1: Var2 (x '=' y) = y by Th1;
 ( x '=' y is being_equality & Var1 (x '=' y) = x ) by Th1, ZF_LANG:5;
hence  Free (x '=' y) = {x,y} by A1, ZF_MODEL:1; ::_thesis: verum
end;

theorem Th59: :: ZF_LANG1:59
for x, y being Variable holds Free (x 'in' y) = {x,y}
proof
let x, y be Variable; ::_thesis: Free (x 'in' y) = {x,y}
A1: Var2 (x 'in' y) = y by Th2;
 ( x 'in' y is being_membership & Var1 (x 'in' y) = x ) by Th2, ZF_LANG:5;
hence  Free (x 'in' y) = {x,y} by A1, ZF_MODEL:1; ::_thesis: verum
end;

theorem Th60: :: ZF_LANG1:60
for p being ZF-formula holds Free ('not' p) = Free p
proof
let p be ZF-formula; ::_thesis: Free ('not' p) = Free p
 ( 'not' p is negative & the_argument_of ('not' p) = p ) by Th3, ZF_LANG:5;
hence  Free ('not' p) = Free p by ZF_MODEL:1; ::_thesis: verum
end;

theorem Th61: :: ZF_LANG1:61
for p, q being ZF-formula holds Free (p '&' q) = (Free p) \/ (Free q)
proof
let p, q be ZF-formula; ::_thesis: Free (p '&' q) = (Free p) \/ (Free q)
A1: the_right_argument_of (p '&' q) = q by Th4;
 ( p '&' q is conjunctive & the_left_argument_of (p '&' q) = p ) by Th4, ZF_LANG:5;
hence  Free (p '&' q) = (Free p) \/ (Free q) by A1, ZF_MODEL:1; ::_thesis: verum
end;

theorem Th62: :: ZF_LANG1:62
for p being ZF-formula
for x being Variable holds Free (All (x,p)) = (Free p) \ {x}
proof
let p be ZF-formula; ::_thesis: for x being Variable holds Free (All (x,p)) = (Free p) \ {x}
let x be Variable; ::_thesis: Free (All (x,p)) = (Free p) \ {x}
A1: the_scope_of (All (x,p)) = p by Th8;
 ( All (x,p) is universal & bound_in (All (x,p)) = x ) by Th8, ZF_LANG:5;
hence  Free (All (x,p)) = (Free p) \ {x} by A1, ZF_MODEL:1; ::_thesis: verum
end;

theorem :: ZF_LANG1:63
for p, q being ZF-formula holds Free (p 'or' q) = (Free p) \/ (Free q)
proof
let p, q be ZF-formula; ::_thesis: Free (p 'or' q) = (Free p) \/ (Free q)
thus  Free (p 'or' q) = Free (('not' p) '&' ('not' q)) by Th60
.= (Free ('not' p)) \/ (Free ('not' q)) by Th61
.= (Free p) \/ (Free ('not' q)) by Th60
.= (Free p) \/ (Free q) by Th60 ; ::_thesis: verum
end;

theorem Th64: :: ZF_LANG1:64
for p, q being ZF-formula holds Free (p => q) = (Free p) \/ (Free q)
proof
let p, q be ZF-formula; ::_thesis: Free (p => q) = (Free p) \/ (Free q)
thus  Free (p => q) = Free (p '&' ('not' q)) by Th60
.= (Free p) \/ (Free ('not' q)) by Th61
.= (Free p) \/ (Free q) by Th60 ; ::_thesis: verum
end;

theorem :: ZF_LANG1:65
for p, q being ZF-formula holds Free (p <=> q) = (Free p) \/ (Free q)
proof
let p, q be ZF-formula; ::_thesis: Free (p <=> q) = (Free p) \/ (Free q)
thus  Free (p <=> q) = (Free (p => q)) \/ (Free (q => p)) by Th61
.= ((Free p) \/ (Free q)) \/ (Free (q => p)) by Th64
.= ((Free p) \/ (Free q)) \/ ((Free q) \/ (Free p)) by Th64
.= (((Free p) \/ (Free q)) \/ (Free q)) \/ (Free p) by XBOOLE_1:4
.= ((Free p) \/ ((Free q) \/ (Free q))) \/ (Free p) by XBOOLE_1:4
.= ((Free p) \/ (Free p)) \/ (Free q) by XBOOLE_1:4
.= (Free p) \/ (Free q) ; ::_thesis: verum
end;

theorem Th66: :: ZF_LANG1:66
for p being ZF-formula
for x being Variable holds Free (Ex (x,p)) = (Free p) \ {x}
proof
let p be ZF-formula; ::_thesis: for x being Variable holds Free (Ex (x,p)) = (Free p) \ {x}
let x be Variable; ::_thesis: Free (Ex (x,p)) = (Free p) \ {x}
thus  Free (Ex (x,p)) = Free (All (x,('not' p))) by Th60
.= (Free ('not' p)) \ {x} by Th62
.= (Free p) \ {x} by Th60 ; ::_thesis: verum
end;

theorem Th67: :: ZF_LANG1:67
for p being ZF-formula
for x, y being Variable holds Free (All (x,y,p)) = (Free p) \ {x,y}
proof
let p be ZF-formula; ::_thesis: for x, y being Variable holds Free (All (x,y,p)) = (Free p) \ {x,y}
let x, y be Variable; ::_thesis: Free (All (x,y,p)) = (Free p) \ {x,y}
thus  Free (All (x,y,p)) = (Free (All (y,p))) \ {x} by Th62
.= ((Free p) \ {y}) \ {x} by Th62
.= (Free p) \ ({x} \/ {y}) by XBOOLE_1:41
.= (Free p) \ {x,y} by ENUMSET1:1 ; ::_thesis: verum
end;

theorem :: ZF_LANG1:68
for p being ZF-formula
for x, y, z being Variable holds Free (All (x,y,z,p)) = (Free p) \ {x,y,z}
proof
let p be ZF-formula; ::_thesis: for x, y, z being Variable holds Free (All (x,y,z,p)) = (Free p) \ {x,y,z}
let x, y, z be Variable; ::_thesis: Free (All (x,y,z,p)) = (Free p) \ {x,y,z}
thus  Free (All (x,y,z,p)) = (Free (All (y,z,p))) \ {x} by Th62
.= ((Free p) \ {y,z}) \ {x} by Th67
.= (Free p) \ ({x} \/ {y,z}) by XBOOLE_1:41
.= (Free p) \ {x,y,z} by ENUMSET1:2 ; ::_thesis: verum
end;

theorem Th69: :: ZF_LANG1:69
for p being ZF-formula
for x, y being Variable holds Free (Ex (x,y,p)) = (Free p) \ {x,y}
proof
let p be ZF-formula; ::_thesis: for x, y being Variable holds Free (Ex (x,y,p)) = (Free p) \ {x,y}
let x, y be Variable; ::_thesis: Free (Ex (x,y,p)) = (Free p) \ {x,y}
thus  Free (Ex (x,y,p)) = (Free (Ex (y,p))) \ {x} by Th66
.= ((Free p) \ {y}) \ {x} by Th66
.= (Free p) \ ({x} \/ {y}) by XBOOLE_1:41
.= (Free p) \ {x,y} by ENUMSET1:1 ; ::_thesis: verum
end;

theorem :: ZF_LANG1:70
for p being ZF-formula
for x, y, z being Variable holds Free (Ex (x,y,z,p)) = (Free p) \ {x,y,z}
proof
let p be ZF-formula; ::_thesis: for x, y, z being Variable holds Free (Ex (x,y,z,p)) = (Free p) \ {x,y,z}
let x, y, z be Variable; ::_thesis: Free (Ex (x,y,z,p)) = (Free p) \ {x,y,z}
thus  Free (Ex (x,y,z,p)) = (Free (Ex (y,z,p))) \ {x} by Th66
.= ((Free p) \ {y,z}) \ {x} by Th69
.= (Free p) \ ({x} \/ {y,z}) by XBOOLE_1:41
.= (Free p) \ {x,y,z} by ENUMSET1:2 ; ::_thesis: verum
end;

scheme :: ZF_LANG1:sch 1
ZFInduction{ P1[ ZF-formula] } :
 for H being ZF-formula holds P1[H]
provided
A1: for x1, x2 being Variable holds
( P1[x1 '=' x2] & P1[x1 'in' x2] ) and
A2: for H being ZF-formula st P1[H] holds
P1[ 'not' H] and
A3: for H1, H2 being ZF-formula st P1[H1] & P1[H2] holds
P1[H1 '&' H2] and
A4: for H being ZF-formula
for x being Variable st P1[H] holds
P1[ All (x,H)]
proof
A5: for H being ZF-formula st H is conjunctive & P1[ the_left_argument_of H] & P1[ the_right_argument_of H] holds
P1[H]
proof
let H be ZF-formula; ::_thesis: ( H is conjunctive & P1[ the_left_argument_of H] & P1[ the_right_argument_of H] implies P1[H] )
assume  H is conjunctive ; ::_thesis: ( not P1[ the_left_argument_of H] or not P1[ the_right_argument_of H] or P1[H] )
then  H = (the_left_argument_of H) '&' (the_right_argument_of H) by ZF_LANG:40;
hence  ( not P1[ the_left_argument_of H] or not P1[ the_right_argument_of H] or P1[H] ) by A3; ::_thesis: verum
end;
A6: for H being ZF-formula st H is atomic holds
P1[H]
proof
let H be ZF-formula; ::_thesis: ( H is atomic implies P1[H] )
assume A7: ( H is being_equality or H is being_membership ) ; :: according to ZF_LANG:def_15 ::_thesis: P1[H]
A8: ( H is being_membership implies P1[H] )
proof
given x1, x2 being Variable such that A9: H = x1 'in' x2 ; :: according to ZF_LANG:def_11 ::_thesis: P1[H]
thus  P1[H] by A1, A9; ::_thesis: verum
end;
 ( H is being_equality implies P1[H] )
proof
given x1, x2 being Variable such that A10: H = x1 '=' x2 ; :: according to ZF_LANG:def_10 ::_thesis: P1[H]
thus  P1[H] by A1, A10; ::_thesis: verum
end;
hence  P1[H] by A7, A8; ::_thesis: verum
end;
A11: for H being ZF-formula st H is universal & P1[ the_scope_of H] holds
P1[H]
proof
let H be ZF-formula; ::_thesis: ( H is universal & P1[ the_scope_of H] implies P1[H] )
assume  H is universal ; ::_thesis: ( not P1[ the_scope_of H] or P1[H] )
then  H = All ((bound_in H),(the_scope_of H)) by ZF_LANG:44;
hence  ( not P1[ the_scope_of H] or P1[H] ) by A4; ::_thesis: verum
end;
A12: for H being ZF-formula st H is negative & P1[ the_argument_of H] holds
P1[H]
proof
let H be ZF-formula; ::_thesis: ( H is negative & P1[ the_argument_of H] implies P1[H] )
assume  H is negative ; ::_thesis: ( not P1[ the_argument_of H] or P1[H] )
then  H = 'not' (the_argument_of H) by ZF_LANG:def_30;
hence  ( not P1[ the_argument_of H] or P1[H] ) by A2; ::_thesis: verum
end;
thus  for H being ZF-formula holds P1[H] from ZF_LANG:sch_1(A6, A12, A5, A11); ::_thesis: verum
end;


definition
let D, D1, D2 be non empty set ;
let f be Function of D,D1;
assume A1: D1 c= D2 ;
funcD2 ! f ->  Function of D,D2 equals :: ZF_LANG1:def 1
f;
correctness
coherence
f is Function of D,D2;
proof
 rng f c= D1 by RELAT_1:def_19;
then A2: rng f c= D2 by A1, XBOOLE_1:1;
 dom f = D by FUNCT_2:def_1;
hence  f is Function of D,D2 by A2, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum
end;
end;

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

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

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

theorem Th71: :: ZF_LANG1:71
for H being ZF-formula
for x being Variable
for M being non empty set
for v being Function of VAR,M holds
( M,v |= All (x,H) iff for m being Element of M holds M,v / (x,m) |= H )
proof
let H be ZF-formula; ::_thesis: 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 )
let x be Variable; ::_thesis: 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 )
let M be non empty set ; ::_thesis: 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 )
let v be Function of VAR,M; ::_thesis: ( M,v |= All (x,H) iff for m being Element of M holds M,v / (x,m) |= H )
thus  ( M,v |= All (x,H) implies for m being Element of M holds M,v / (x,m) |= H ) ::_thesis: ( ( for m being Element of M holds M,v / (x,m) |= H ) implies M,v |= All (x,H) )
proof
assume A1: M,v |= All (x,H) ; ::_thesis: for m being Element of M holds M,v / (x,m) |= H
let m be Element of M; ::_thesis: M,v / (x,m) |= H
 for y being Variable st (v / (x,m)) . y <> v . y holds
x = y by FUNCT_7:32;
hence  M,v / (x,m) |= H by A1, ZF_MODEL:16; ::_thesis: verum
end;
assume A2: for m being Element of M holds M,v / (x,m) |= H ; ::_thesis: M,v |= All (x,H)
now__::_thesis:_for_v9_being_Function_of_VAR,M_st_(_for_y_being_Variable_st_v9_._y_<>_v_._y_holds_
x_=_y_)_holds_
M,v9_|=_H
let v9 be Function of VAR,M; ::_thesis: ( ( for y being Variable st v9 . y <> v . y holds
x = y ) implies M,v9 |= H )
assume  for y being Variable st v9 . y <> v . y holds
x = y ; ::_thesis: M,v9 |= H
then  v9 = v / (x,(v9 . x)) by FUNCT_7:129;
hence  M,v9 |= H by A2; ::_thesis: verum
end;
hence  M,v |= All (x,H) by ZF_MODEL:16; ::_thesis: verum
end;

theorem Th72: :: ZF_LANG1:72
for H being ZF-formula
for x being Variable
for M being non empty set
for m being Element of M
for v being Function of VAR,M holds
( M,v |= All (x,H) iff M,v / (x,m) |= All (x,H) )
proof
let H be ZF-formula; ::_thesis: 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) )
let x be Variable; ::_thesis: 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) )
let M be non empty set ; ::_thesis: 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) )
let m be Element of M; ::_thesis: for v being Function of VAR,M holds
( M,v |= All (x,H) iff M,v / (x,m) |= All (x,H) )
let v be Function of VAR,M; ::_thesis: ( M,v |= All (x,H) iff M,v / (x,m) |= All (x,H) )
A1: for v being Function of VAR,M
for m being Element of M st M,v |= All (x,H) holds
M,v / (x,m) |= All (x,H)
proof
let v be Function of VAR,M; ::_thesis: for m being Element of M st M,v |= All (x,H) holds
M,v / (x,m) |= All (x,H)
let m be Element of M; ::_thesis: ( M,v |= All (x,H) implies M,v / (x,m) |= All (x,H) )
assume A2: M,v |= All (x,H) ; ::_thesis: M,v / (x,m) |= All (x,H)
now__::_thesis:_for_m9_being_Element_of_M_holds_M,(v_/_(x,m))_/_(x,m9)_|=_H
let m9 be Element of M; ::_thesis: M,(v / (x,m)) / (x,m9) |= H
 (v / (x,m)) / (x,m9) = v / (x,m9) by FUNCT_7:34;
hence  M,(v / (x,m)) / (x,m9) |= H by A2, Th71; ::_thesis: verum
end;
hence  M,v / (x,m) |= All (x,H) by Th71; ::_thesis: verum
end;
(v / (x,m)) / (x,(v . x)) = v / (x,(v . x)) by FUNCT_7:34
.= v by FUNCT_7:35 ;
hence  ( M,v |= All (x,H) iff M,v / (x,m) |= All (x,H) ) by A1; ::_thesis: verum
end;

theorem Th73: :: ZF_LANG1:73
for H being ZF-formula
for x being Variable
for M being non empty set
for v being Function of VAR,M holds
( M,v |= Ex (x,H) iff ex m being Element of M st M,v / (x,m) |= H )
proof
let H be ZF-formula; ::_thesis: 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 )
let x be Variable; ::_thesis: 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 )
let M be non empty set ; ::_thesis: 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 )
let v be Function of VAR,M; ::_thesis: ( M,v |= Ex (x,H) iff ex m being Element of M st M,v / (x,m) |= H )
thus  ( M,v |= Ex (x,H) implies ex m being Element of M st M,v / (x,m) |= H ) ::_thesis: ( ex m being Element of M st M,v / (x,m) |= H implies M,v |= Ex (x,H) )
proof
assume  M,v |= Ex (x,H) ; ::_thesis: ex m being Element of M st M,v / (x,m) |= H
then consider v9 being Function of VAR,M such that
A1: ( ( for y being Variable st v9 . y <> v . y holds
x = y ) & M,v9 |= H ) by ZF_MODEL:20;
take  v9 . x ; ::_thesis: M,v / (x,(v9 . x)) |= H
thus  M,v / (x,(v9 . x)) |= H by A1, FUNCT_7:129; ::_thesis: verum
end;
given m being Element of M such that A2: M,v / (x,m) |= H ; ::_thesis: M,v |= Ex (x,H)
now__::_thesis:_ex_v9_being_Function_of_VAR,M_st_
(_(_for_y_being_Variable_st_v9_._y_<>_v_._y_holds_
x_=_y_)_&_M,v9_|=_H_)
take v9 = v / (x,m); ::_thesis: ( ( for y being Variable st v9 . y <> v . y holds
x = y ) & M,v9 |= H )
thus  for y being Variable st v9 . y <> v . y holds
x = y by FUNCT_7:32; ::_thesis: M,v9 |= H
thus  M,v9 |= H by A2; ::_thesis: verum
end;
hence  M,v |= Ex (x,H) by ZF_MODEL:20; ::_thesis: verum
end;

theorem :: ZF_LANG1:74
for H being ZF-formula
for x being Variable
for M being non empty set
for m being Element of M
for v being Function of VAR,M holds
( M,v |= Ex (x,H) iff M,v / (x,m) |= Ex (x,H) )
proof
let H be ZF-formula; ::_thesis: 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) )
let x be Variable; ::_thesis: 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) )
let M be non empty set ; ::_thesis: 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) )
let m be Element of M; ::_thesis: for v being Function of VAR,M holds
( M,v |= Ex (x,H) iff M,v / (x,m) |= Ex (x,H) )
let v be Function of VAR,M; ::_thesis: ( M,v |= Ex (x,H) iff M,v / (x,m) |= Ex (x,H) )
A1: for v being Function of VAR,M
for m being Element of M st M,v |= Ex (x,H) holds
M,v / (x,m) |= Ex (x,H)
proof
let v be Function of VAR,M; ::_thesis: for m being Element of M st M,v |= Ex (x,H) holds
M,v / (x,m) |= Ex (x,H)
let m be Element of M; ::_thesis: ( M,v |= Ex (x,H) implies M,v / (x,m) |= Ex (x,H) )
assume  M,v |= Ex (x,H) ; ::_thesis: M,v / (x,m) |= Ex (x,H)
then consider m9 being Element of M such that
A2: M,v / (x,m9) |= H by Th73;
 (v / (x,m)) / (x,m9) = v / (x,m9) by FUNCT_7:34;
hence  M,v / (x,m) |= Ex (x,H) by A2, Th73; ::_thesis: verum
end;
(v / (x,m)) / (x,(v . x)) = v / (x,(v . x)) by FUNCT_7:34
.= v by FUNCT_7:35 ;
hence  ( M,v |= Ex (x,H) iff M,v / (x,m) |= Ex (x,H) ) by A1; ::_thesis: verum
end;

theorem :: ZF_LANG1:75
for H being ZF-formula
for M being non empty set
for v, v9 being Function of VAR,M st ( for x being Variable st x in Free H holds
v9 . x = v . x ) & M,v |= H holds
M,v9 |= H
proof
let H be ZF-formula; ::_thesis: 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
let M be non empty set ; ::_thesis: 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
defpred S1[ ZF-formula] means  for v, v9 being Function of VAR,M st ( for x being Variable st x in Free $1 holds
v9 . x = v . x ) & M,v |= $1 holds
M,v9 |= $1;
A1: for H1, H2 being ZF-formula st S1[H1] & S1[H2] holds
S1[H1 '&' H2]
proof
let H1, H2 be ZF-formula; ::_thesis: ( S1[H1] & S1[H2] implies S1[H1 '&' H2] )
assume that
A2: S1[H1] and
A3: S1[H2] ; ::_thesis: S1[H1 '&' H2]
let v, v9 be Function of VAR,M; ::_thesis: ( ( for x being Variable st x in Free (H1 '&' H2) holds
v9 . x = v . x ) & M,v |= H1 '&' H2 implies M,v9 |= H1 '&' H2 )
assume A4: for x being Variable st x in Free (H1 '&' H2) holds
v9 . x = v . x ; ::_thesis: ( not M,v |= H1 '&' H2 or M,v9 |= H1 '&' H2 )
A5: Free (H1 '&' H2) = (Free H1) \/ (Free H2) by Th61;
A6: now__::_thesis:_for_x_being_Variable_st_x_in_Free_H2_holds_
v9_._x_=_v_._x
let x be Variable; ::_thesis: ( x in Free H2 implies v9 . x = v . x )
assume  x in Free H2 ; ::_thesis: v9 . x = v . x
then  x in Free (H1 '&' H2) by A5, XBOOLE_0:def_3;
hence  v9 . x = v . x by A4; ::_thesis: verum
end;
assume A7: M,v |= H1 '&' H2 ; ::_thesis: M,v9 |= H1 '&' H2
then  M,v |= H2 by ZF_MODEL:15;
then A8: M,v9 |= H2 by A3, A6;
A9: now__::_thesis:_for_x_being_Variable_st_x_in_Free_H1_holds_
v9_._x_=_v_._x
let x be Variable; ::_thesis: ( x in Free H1 implies v9 . x = v . x )
assume  x in Free H1 ; ::_thesis: v9 . x = v . x
then  x in Free (H1 '&' H2) by A5, XBOOLE_0:def_3;
hence  v9 . x = v . x by A4; ::_thesis: verum
end;
 M,v |= H1 by A7, ZF_MODEL:15;
then  M,v9 |= H1 by A2, A9;
hence  M,v9 |= H1 '&' H2 by A8, ZF_MODEL:15; ::_thesis: verum
end;
A10: for x1, x2 being Variable holds
( S1[x1 '=' x2] & S1[x1 'in' x2] )
proof
let x1, x2 be Variable; ::_thesis: ( S1[x1 '=' x2] & S1[x1 'in' x2] )
A11: Free (x1 '=' x2) = {x1,x2} by Th58;
thus  S1[x1 '=' x2] ::_thesis: S1[x1 'in' x2]
proof
let v, v9 be Function of VAR,M; ::_thesis: ( ( for x being Variable st x in Free (x1 '=' x2) holds
v9 . x = v . x ) & M,v |= x1 '=' x2 implies M,v9 |= x1 '=' x2 )
assume A12: for x being Variable st x in Free (x1 '=' x2) holds
v9 . x = v . x ; ::_thesis: ( not M,v |= x1 '=' x2 or M,v9 |= x1 '=' x2 )
 x2 in Free (x1 '=' x2) by A11, TARSKI:def_2;
then A13: v9 . x2 = v . x2 by A12;
assume  M,v |= x1 '=' x2 ; ::_thesis: M,v9 |= x1 '=' x2
then A14: v . x1 = v . x2 by ZF_MODEL:12;
 x1 in Free (x1 '=' x2) by A11, TARSKI:def_2;
then  v9 . x1 = v . x1 by A12;
hence  M,v9 |= x1 '=' x2 by A14, A13, ZF_MODEL:12; ::_thesis: verum
end;
let v, v9 be Function of VAR,M; ::_thesis: ( ( for x being Variable st x in Free (x1 'in' x2) holds
v9 . x = v . x ) & M,v |= x1 'in' x2 implies M,v9 |= x1 'in' x2 )
assume A15: for x being Variable st x in Free (x1 'in' x2) holds
v9 . x = v . x ; ::_thesis: ( not M,v |= x1 'in' x2 or M,v9 |= x1 'in' x2 )
A16: Free (x1 'in' x2) = {x1,x2} by Th59;
then  x2 in Free (x1 'in' x2) by TARSKI:def_2;
then A17: v9 . x2 = v . x2 by A15;
assume  M,v |= x1 'in' x2 ; ::_thesis: M,v9 |= x1 'in' x2
then A18: v . x1 in v . x2 by ZF_MODEL:13;
 x1 in Free (x1 'in' x2) by A16, TARSKI:def_2;
then  v9 . x1 = v . x1 by A15;
hence  M,v9 |= x1 'in' x2 by A18, A17, ZF_MODEL:13; ::_thesis: verum
end;
A19: for H being ZF-formula
for x being Variable st S1[H] holds
S1[ All (x,H)]
proof
let H be ZF-formula; ::_thesis: for x being Variable st S1[H] holds
S1[ All (x,H)]
let x1 be Variable; ::_thesis: ( S1[H] implies S1[ All (x1,H)] )
assume A20: S1[H] ; ::_thesis: S1[ All (x1,H)]
let v, v9 be Function of VAR,M; ::_thesis: ( ( for x being Variable st x in Free (All (x1,H)) holds
v9 . x = v . x ) & M,v |= All (x1,H) implies M,v9 |= All (x1,H) )
assume that
A21: for x being Variable st x in Free (All (x1,H)) holds
v9 . x = v . x and
A22: M,v |= All (x1,H) ; ::_thesis: M,v9 |= All (x1,H)
now__::_thesis:_for_m_being_Element_of_M_holds_M,v9_/_(x1,m)_|=_H
let m be Element of M; ::_thesis: M,v9 / (x1,m) |= H
A23: Free (All (x1,H)) = (Free H) \ {x1} by Th62;
A24: now__::_thesis:_for_x_being_Variable_st_x_in_Free_H_holds_
(v9_/_(x1,m))_._x_=_(v_/_(x1,m))_._x
let x be Variable; ::_thesis: ( x in Free H implies (v9 / (x1,m)) . x = (v / (x1,m)) . x )
assume  x in Free H ; ::_thesis: (v9 / (x1,m)) . x = (v / (x1,m)) . x
then  ( ( x in Free (All (x1,H)) & not x in {x1} ) or x in {x1} ) by A23, XBOOLE_0:def_5;
then  ( ( v9 . x = v . x & x <> x1 ) or x = x1 ) by A21, TARSKI:def_1;
then  ( ( (v9 / (x1,m)) . x = v . x & v . x = (v / (x1,m)) . x ) or ( (v / (x1,m)) . x = m & (v9 / (x1,m)) . x = m ) ) by FUNCT_7:32, FUNCT_7:128;
hence  (v9 / (x1,m)) . x = (v / (x1,m)) . x ; ::_thesis: verum
end;
 M,v / (x1,m) |= H by A22, Th71;
hence  M,v9 / (x1,m) |= H by A20, A24; ::_thesis: verum
end;
hence  M,v9 |= All (x1,H) by Th71; ::_thesis: verum
end;
A25: for H being ZF-formula st S1[H] holds
S1[ 'not' H]
proof
let H be ZF-formula; ::_thesis: ( S1[H] implies S1[ 'not' H] )
assume A26: S1[H] ; ::_thesis: S1[ 'not' H]
let v, v9 be Function of VAR,M; ::_thesis: ( ( for x being Variable st x in Free ('not' H) holds
v9 . x = v . x ) & M,v |= 'not' H implies M,v9 |= 'not' H )
assume A27: for x being Variable st x in Free ('not' H) holds
v9 . x = v . x ; ::_thesis: ( not M,v |= 'not' H or M,v9 |= 'not' H )
A28: now__::_thesis:_for_x_being_Variable_st_x_in_Free_H_holds_
v_._x_=_v9_._x
let x be Variable; ::_thesis: ( x in Free H implies v . x = v9 . x )
assume  x in Free H ; ::_thesis: v . x = v9 . x
then  x in Free ('not' H) by Th60;
hence  v . x = v9 . x by A27; ::_thesis: verum
end;
assume  M,v |= 'not' H ; ::_thesis: M,v9 |= 'not' H
then  not M,v |= H by ZF_MODEL:14;
then  not M,v9 |= H by A26, A28;
hence  M,v9 |= 'not' H by ZF_MODEL:14; ::_thesis: verum
end;
 for H being ZF-formula holds S1[H] from ZF_LANG1:sch_1(A10, A25, A1, A19);
hence  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 ; ::_thesis: verum
end;

registration
let H be ZF-formula;
cluster Free H ->  finite ;
coherence
 Free H is finite
proof
defpred S1[ ZF-formula] means  Free H is finite ;
A1: for p, q being ZF-formula st S1[p] & S1[q] holds
S1[p '&' q]
proof
let p, q be ZF-formula; ::_thesis: ( S1[p] & S1[q] implies S1[p '&' q] )
 Free (p '&' q) = (Free p) \/ (Free q) by Th61;
hence  ( S1[p] & S1[q] implies S1[p '&' q] ) ; ::_thesis: verum
end;
A2: for p being ZF-formula
for x being Variable st S1[p] holds
S1[ All (x,p)]
proof
let p be ZF-formula; ::_thesis: for x being Variable st S1[p] holds
S1[ All (x,p)]
let x be Variable; ::_thesis: ( S1[p] implies S1[ All (x,p)] )
 Free (All (x,p)) = (Free p) \ {x} by Th62;
hence  ( S1[p] implies S1[ All (x,p)] ) ; ::_thesis: verum
end;
A3: for x, y being Variable holds
( S1[x '=' y] & S1[x 'in' y] )
proof
let x, y be Variable; ::_thesis: ( S1[x '=' y] & S1[x 'in' y] )
 Free (x '=' y) = {x,y} by Th58;
hence  ( S1[x '=' y] & S1[x 'in' y] ) by Th59; ::_thesis: verum
end;
A4: for p being ZF-formula st S1[p] holds
S1[ 'not' p] by Th60;
 for p being ZF-formula holds S1[p] from ZF_LANG1:sch_1(A3, A4, A1, A2);
hence  Free H is finite ; ::_thesis: verum
end;
end;


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

theorem :: ZF_LANG1:77
for x being Variable ex i being Element of NAT st x = x. i
proof
let x be Variable; ::_thesis: ex i being Element of NAT st x = x. i
 x in VAR ;
then consider j being Element of NAT  such that
A1: x = j and
A2: 5 <= j ;
consider i being Nat such that
A3: j = 5 + i by A2, NAT_1:10;
reconsider i = i as Element of NAT by ORDINAL1:def_12;
take  i ; ::_thesis: x = x. i
thus  x = x. i by A1, A3; ::_thesis: verum
end;

theorem Th78: :: ZF_LANG1:78
for x being Variable
for M being non empty set
for v being Function of VAR,M holds M,v |= x '=' x
proof
let x be Variable; ::_thesis: for M being non empty set
for v being Function of VAR,M holds M,v |= x '=' x
let M be non empty set ; ::_thesis: for v being Function of VAR,M holds M,v |= x '=' x
let v be Function of VAR,M; ::_thesis: M,v |= x '=' x
 v . x = v . x ;
hence  M,v |= x '=' x by ZF_MODEL:12; ::_thesis: verum
end;

theorem Th79: :: ZF_LANG1:79
for x being Variable
for M being non empty set holds M |= x '=' x
proof
let x be Variable; ::_thesis: for M being non empty set holds M |= x '=' x
let M be non empty set ; ::_thesis: M |= x '=' x
 for v being Function of VAR,M holds M,v |= x '=' x by Th78;
hence  M |= x '=' x by ZF_MODEL:def_5; ::_thesis: verum
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
proof
let x be Variable; ::_thesis: for M being non empty set
for v being Function of VAR,M holds not M,v |= x 'in' x
let M be non empty set ; ::_thesis: for v being Function of VAR,M holds not M,v |= x 'in' x
let v be Function of VAR,M; ::_thesis: not M,v |= x 'in' x
 not v . x in v . x ;
hence  not M,v |= x 'in' x by ZF_MODEL:13; ::_thesis: verum
end;

theorem Th81: :: ZF_LANG1:81
for x being Variable
for M being non empty set holds
( not M |= x 'in' x & M |= 'not' (x 'in' x) )
proof
let x be Variable; ::_thesis: for M being non empty set holds
( not M |= x 'in' x & M |= 'not' (x 'in' x) )
let M be non empty set ; ::_thesis: ( not M |= x 'in' x & M |= 'not' (x 'in' x) )
set v = the Function of VAR,M;
 not M, the Function of VAR,M |= x 'in' x by Th80;
hence  not M |= x 'in' x by ZF_MODEL:def_5; ::_thesis: M |= 'not' (x 'in' x)
let v be Function of VAR,M; :: according to ZF_MODEL:def_5 ::_thesis: M,v |= 'not' (x 'in' x)
 not M,v |= x 'in' x by Th80;
hence  M,v |= 'not' (x 'in' x) by ZF_MODEL:14; ::_thesis: verum
end;

theorem :: ZF_LANG1:82
for x, y being Variable
for M being non empty set holds
( M |= x '=' y iff ( x = y or ex a being set st {a} = M ) )
proof
let x, y be Variable; ::_thesis: for M being non empty set holds
( M |= x '=' y iff ( x = y or ex a being set st {a} = M ) )
let M be non empty set ; ::_thesis: ( M |= x '=' y iff ( x = y or ex a being set st {a} = M ) )
thus  ( not M |= x '=' y or x = y or ex a being set st {a} = M ) ::_thesis: ( ( x = y or ex a being set st {a} = M ) implies M |= x '=' y )
proof
set v = the Function of VAR,M;
set m = the Element of M;
assume that
A1: for v being Function of VAR,M holds M,v |= x '=' y and
A2: x <> y ; :: according to ZF_MODEL:def_5 ::_thesis: ex a being set st {a} = M
reconsider a = the Element of M as set ;
take  a ; ::_thesis: {a} = M
thus  {a} c= M by ZFMISC_1:31; :: according to XBOOLE_0:def_10 ::_thesis: M c= {a}
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in M or b in {a} )
assume that
A3: b in M and
A4: not b in {a} ; ::_thesis: contradiction
reconsider b = b as Element of M by A3;
 M,( the Function of VAR,M / (x, the Element of M)) / (y,b) |= x '=' y by A1;
then A5: (( the Function of VAR,M / (x, the Element of M)) / (y,b)) . x = (( the Function of VAR,M / (x, the Element of M)) / (y,b)) . y by ZF_MODEL:12;
A6: ( ( the Function of VAR,M / (x, the Element of M)) . x = the Element of M & (( the Function of VAR,M / (x, the Element of M)) / (y,b)) . y = b ) by FUNCT_7:128;
 (( the Function of VAR,M / (x, the Element of M)) / (y,b)) . x = ( the Function of VAR,M / (x, the Element of M)) . x by A2, FUNCT_7:32;
hence  contradiction by A4, A5, A6, TARSKI:def_1; ::_thesis: verum
end;
now__::_thesis:_(_ex_a_being_set_st_{a}_=_M_implies_for_v_being_Function_of_VAR,M_holds_M,v_|=_x_'='_y_)
given a being set  such that A7: {a} = M ; ::_thesis: for v being Function of VAR,M holds M,v |= x '=' y
let v be Function of VAR,M; ::_thesis: M,v |= x '=' y
 ( v . x = a & v . y = a ) by A7, TARSKI:def_1;
hence  M,v |= x '=' y by ZF_MODEL:12; ::_thesis: verum
end;
hence  ( ( x = y or ex a being set st {a} = M ) implies M |= x '=' y ) by Th79, ZF_MODEL:def_5; ::_thesis: verum
end;

theorem :: ZF_LANG1:83
for x, y being Variable
for M being non empty set holds
( M |= 'not' (x 'in' y) iff ( x = y or for X being set st X in M holds
X misses M ) )
proof
let x, y be Variable; ::_thesis: 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 ) )
let M be non empty set ; ::_thesis: ( M |= 'not' (x 'in' y) iff ( x = y or for X being set st X in M holds
X misses M ) )
thus  ( not M |= 'not' (x 'in' y) or x = y or for X being set st X in M holds
X misses M ) ::_thesis: ( ( x = y or for X being set st X in M holds
X misses M ) implies M |= 'not' (x 'in' y) )
proof
set v = the Function of VAR,M;
assume that
A1: for v being Function of VAR,M holds M,v |= 'not' (x 'in' y) and
A2: x <> y ; :: according to ZF_MODEL:def_5 ::_thesis: for X being set st X in M holds
X misses M
let X be set ; ::_thesis: ( X in M implies X misses M )
set a = the Element of X /\ M;
assume  X in M ; ::_thesis: X misses M
then reconsider m = X as Element of M ;
assume A3: X /\ M <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction
then reconsider a = the Element of X /\ M as Element of M by XBOOLE_0:def_4;
 M,( the Function of VAR,M / (x,a)) / (y,m) |= 'not' (x 'in' y) by A1;
then  not M,( the Function of VAR,M / (x,a)) / (y,m) |= x 'in' y by ZF_MODEL:14;
then A4: not (( the Function of VAR,M / (x,a)) / (y,m)) . x in (( the Function of VAR,M / (x,a)) / (y,m)) . y by ZF_MODEL:13;
A5: ( ( the Function of VAR,M / (x,a)) . x = a & (( the Function of VAR,M / (x,a)) / (y,m)) . y = m ) by FUNCT_7:128;
 (( the Function of VAR,M / (x,a)) / (y,m)) . x = ( the Function of VAR,M / (x,a)) . x by A2, FUNCT_7:32;
hence  contradiction by A3, A4, A5, XBOOLE_0:def_4; ::_thesis: verum
end;
now__::_thesis:_(_(_for_X_being_set_st_X_in_M_holds_
X_misses_M_)_implies_for_v_being_Function_of_VAR,M_holds_M,v_|=_'not'_(x_'in'_y)_)
assume A6: for X being set st X in M holds
X misses M ; ::_thesis: for v being Function of VAR,M holds M,v |= 'not' (x 'in' y)
let v be Function of VAR,M; ::_thesis: M,v |= 'not' (x 'in' y)
 v . y misses M by A6;
then  not v . x in v . y by XBOOLE_0:3;
then  not M,v |= x 'in' y by ZF_MODEL:13;
hence  M,v |= 'not' (x 'in' y) by ZF_MODEL:14; ::_thesis: verum
end;
hence  ( ( x = y or for X being set st X in M holds
X misses M ) implies M |= 'not' (x 'in' y) ) by Th81, ZF_MODEL:def_5; ::_thesis: verum
end;

theorem :: ZF_LANG1:84
for H being ZF-formula
for M being non empty set
for v being Function of VAR,M st H is being_equality holds
( M,v |= H iff v . (Var1 H) = v . (Var2 H) )
proof
let H be ZF-formula; ::_thesis: 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) )
let M be non empty set ; ::_thesis: for v being Function of VAR,M st H is being_equality holds
( M,v |= H iff v . (Var1 H) = v . (Var2 H) )
let v be Function of VAR,M; ::_thesis: ( H is being_equality implies ( M,v |= H iff v . (Var1 H) = v . (Var2 H) ) )
assume  H is being_equality ; ::_thesis: ( M,v |= H iff v . (Var1 H) = v . (Var2 H) )
then  H = (Var1 H) '=' (Var2 H) by ZF_LANG:36;
hence  ( M,v |= H iff v . (Var1 H) = v . (Var2 H) ) by ZF_MODEL:12; ::_thesis: verum
end;

theorem :: ZF_LANG1:85
for H being ZF-formula
for M being non empty set
for v being Function of VAR,M st H is being_membership holds
( M,v |= H iff v . (Var1 H) in v . (Var2 H) )
proof
let H be ZF-formula; ::_thesis: 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) )
let M be non empty set ; ::_thesis: for v being Function of VAR,M st H is being_membership holds
( M,v |= H iff v . (Var1 H) in v . (Var2 H) )
let v be Function of VAR,M; ::_thesis: ( H is being_membership implies ( M,v |= H iff v . (Var1 H) in v . (Var2 H) ) )
assume  H is being_membership ; ::_thesis: ( M,v |= H iff v . (Var1 H) in v . (Var2 H) )
then  H = (Var1 H) 'in' (Var2 H) by ZF_LANG:37;
hence  ( M,v |= H iff v . (Var1 H) in v . (Var2 H) ) by ZF_MODEL:13; ::_thesis: verum
end;

theorem :: ZF_LANG1:86
for H being ZF-formula
for M being non empty set
for v being Function of VAR,M st H is negative holds
( M,v |= H iff not M,v |= the_argument_of H )
proof
let H be ZF-formula; ::_thesis: 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 )
let M be non empty set ; ::_thesis: for v being Function of VAR,M st H is negative holds
( M,v |= H iff not M,v |= the_argument_of H )
let v be Function of VAR,M; ::_thesis: ( H is negative implies ( M,v |= H iff not M,v |= the_argument_of H ) )
assume  H is negative ; ::_thesis: ( M,v |= H iff not M,v |= the_argument_of H )
then  H = 'not' (the_argument_of H) by ZF_LANG:def_30;
hence  ( M,v |= H iff not M,v |= the_argument_of H ) by ZF_MODEL:14; ::_thesis: verum
end;

theorem :: ZF_LANG1:87
for H being ZF-formula
for M being non empty set
for v being Function of VAR,M st H is conjunctive holds
( M,v |= H iff ( M,v |= the_left_argument_of H & M,v |= the_right_argument_of H ) )
proof
let H be ZF-formula; ::_thesis: 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 ) )
let M be non empty set ; ::_thesis: 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 ) )
let v be Function of VAR,M; ::_thesis: ( H is conjunctive implies ( M,v |= H iff ( M,v |= the_left_argument_of H & M,v |= the_right_argument_of H ) ) )
assume  H is conjunctive ; ::_thesis: ( M,v |= H iff ( M,v |= the_left_argument_of H & M,v |= the_right_argument_of H ) )
then  H = (the_left_argument_of H) '&' (the_right_argument_of H) by ZF_LANG:40;
hence  ( M,v |= H iff ( M,v |= the_left_argument_of H & M,v |= the_right_argument_of H ) ) by ZF_MODEL:15; ::_thesis: verum
end;

theorem :: ZF_LANG1:88
for H being ZF-formula
for M being non empty set
for v being Function of VAR,M st H is universal holds
( M,v |= H iff for m being Element of M holds M,v / ((bound_in H),m) |= the_scope_of H )
proof
let H be ZF-formula; ::_thesis: 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 )
let M be non empty set ; ::_thesis: 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 )
let v be Function of VAR,M; ::_thesis: ( H is universal implies ( M,v |= H iff for m being Element of M holds M,v / ((bound_in H),m) |= the_scope_of H ) )
assume  H is universal ; ::_thesis: ( M,v |= H iff for m being Element of M holds M,v / ((bound_in H),m) |= the_scope_of H )
then  H = All ((bound_in H),(the_scope_of H)) by ZF_LANG:44;
hence  ( M,v |= H iff for m being Element of M holds M,v / ((bound_in H),m) |= the_scope_of H ) by Th71; ::_thesis: verum
end;

theorem :: ZF_LANG1:89
for H being ZF-formula
for M being non empty set
for v being Function of VAR,M st H is disjunctive holds
( M,v |= H iff ( M,v |= the_left_argument_of H or M,v |= the_right_argument_of H ) )
proof
let H be ZF-formula; ::_thesis: 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 ) )
let M be non empty set ; ::_thesis: 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 ) )
let v be Function of VAR,M; ::_thesis: ( H is disjunctive implies ( M,v |= H iff ( M,v |= the_left_argument_of H or M,v |= the_right_argument_of H ) ) )
assume  H is disjunctive ; ::_thesis: ( M,v |= H iff ( M,v |= the_left_argument_of H or M,v |= the_right_argument_of H ) )
then  H = (the_left_argument_of H) 'or' (the_right_argument_of H) by ZF_LANG:41;
hence  ( M,v |= H iff ( M,v |= the_left_argument_of H or M,v |= the_right_argument_of H ) ) by ZF_MODEL:17; ::_thesis: verum
end;

theorem :: ZF_LANG1:90
for H being ZF-formula
for M being non empty set
for v being Function of VAR,M st H is conditional holds
( M,v |= H iff ( M,v |= the_antecedent_of H implies M,v |= the_consequent_of H ) )
proof
let H be ZF-formula; ::_thesis: 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 ) )
let M be non empty set ; ::_thesis: 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 ) )
let v be Function of VAR,M; ::_thesis: ( H is conditional implies ( M,v |= H iff ( M,v |= the_antecedent_of H implies M,v |= the_consequent_of H ) ) )
assume  H is conditional ; ::_thesis: ( M,v |= H iff ( M,v |= the_antecedent_of H implies M,v |= the_consequent_of H ) )
then  H = (the_antecedent_of H) => (the_consequent_of H) by ZF_LANG:47;
hence  ( M,v |= H iff ( M,v |= the_antecedent_of H implies M,v |= the_consequent_of H ) ) by ZF_MODEL:18; ::_thesis: verum
end;

theorem :: ZF_LANG1:91
for H being ZF-formula
for M being non empty set
for v being Function of VAR,M st H is biconditional holds
( M,v |= H iff ( M,v |= the_left_side_of H iff M,v |= the_right_side_of H ) )
proof
let H be ZF-formula; ::_thesis: 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 ) )
let M be non empty set ; ::_thesis: 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 ) )
let v be Function of VAR,M; ::_thesis: ( H is biconditional implies ( M,v |= H iff ( M,v |= the_left_side_of H iff M,v |= the_right_side_of H ) ) )
assume  H is biconditional ; ::_thesis: ( M,v |= H iff ( M,v |= the_left_side_of H iff M,v |= the_right_side_of H ) )
then  H = (the_left_side_of H) <=> (the_right_side_of H) by ZF_LANG:49;
hence  ( M,v |= H iff ( M,v |= the_left_side_of H iff M,v |= the_right_side_of H ) ) by ZF_MODEL:19; ::_thesis: verum
end;

theorem :: ZF_LANG1:92
for H being ZF-formula
for M being non empty set
for v being Function of VAR,M st H is existential holds
( M,v |= H iff ex m being Element of M st M,v / ((bound_in H),m) |= the_scope_of H )
proof
let H be ZF-formula; ::_thesis: 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 )
let M be non empty set ; ::_thesis: 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 )
let v be Function of VAR,M; ::_thesis: ( H is existential implies ( M,v |= H iff ex m being Element of M st M,v / ((bound_in H),m) |= the_scope_of H ) )
assume  H is existential ; ::_thesis: ( M,v |= H iff ex m being Element of M st M,v / ((bound_in H),m) |= the_scope_of H )
then  H = Ex ((bound_in H),(the_scope_of H)) by ZF_LANG:45;
hence  ( M,v |= H iff ex m being Element of M st M,v / ((bound_in H),m) |= the_scope_of H ) by Th73; ::_thesis: verum
end;

theorem :: ZF_LANG1:93
for H being ZF-formula
for x being Variable
for M being non empty set holds
( M |= Ex (x,H) iff for v being Function of VAR,M ex m being Element of M st M,v / (x,m) |= H )
proof
let H be ZF-formula; ::_thesis: 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 )
let x be Variable; ::_thesis: 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 )
let M be non empty set ; ::_thesis: ( M |= Ex (x,H) iff for v being Function of VAR,M ex m being Element of M st M,v / (x,m) |= H )
thus  ( M |= Ex (x,H) implies for v being Function of VAR,M ex m being Element of M st M,v / (x,m) |= H ) ::_thesis: ( ( for v being Function of VAR,M ex m being Element of M st M,v / (x,m) |= H ) implies M |= Ex (x,H) )
proof
assume A1: for v being Function of VAR,M holds M,v |= Ex (x,H) ; :: according to ZF_MODEL:def_5 ::_thesis: for v being Function of VAR,M ex m being Element of M st M,v / (x,m) |= H
let v be Function of VAR,M; ::_thesis: ex m being Element of M st M,v / (x,m) |= H
 M,v |= Ex (x,H) by A1;
hence  ex m being Element of M st M,v / (x,m) |= H by Th73; ::_thesis: verum
end;
assume A2: for v being Function of VAR,M ex m being Element of M st M,v / (x,m) |= H ; ::_thesis: M |= Ex (x,H)
let v be Function of VAR,M; :: according to ZF_MODEL:def_5 ::_thesis: M,v |= Ex (x,H)
 ex m being Element of M st M,v / (x,m) |= H by A2;
hence  M,v |= Ex (x,H) by Th73; ::_thesis: verum
end;

theorem Th94: :: ZF_LANG1:94
for H being ZF-formula
for x being Variable
for M being non empty set st M |= H holds
M |= Ex (x,H)
proof
let H be ZF-formula; ::_thesis: for x being Variable
for M being non empty set st M |= H holds
M |= Ex (x,H)
let x be Variable; ::_thesis: for M being non empty set st M |= H holds
M |= Ex (x,H)
let M be non empty set ; ::_thesis: ( M |= H implies M |= Ex (x,H) )
assume A1: M |= H ; ::_thesis: M |= Ex (x,H)
let v be Function of VAR,M; :: according to ZF_MODEL:def_5 ::_thesis: M,v |= Ex (x,H)
 M,v / (x,(v . x)) |= H by A1, ZF_MODEL:def_5;
hence  M,v |= Ex (x,H) by Th73; ::_thesis: verum
end;

theorem Th95: :: ZF_LANG1:95
for H being ZF-formula
for x, y being Variable
for M being non empty set holds
( M |= H iff M |= All (x,y,H) )
proof
let H be ZF-formula; ::_thesis: for x, y being Variable
for M being non empty set holds
( M |= H iff M |= All (x,y,H) )
let x, y be Variable; ::_thesis: for M being non empty set holds
( M |= H iff M |= All (x,y,H) )
let M be non empty set ; ::_thesis: ( M |= H iff M |= All (x,y,H) )
 ( M |= H iff M |= All (y,H) ) by ZF_MODEL:23;
hence  ( M |= H iff M |= All (x,y,H) ) by ZF_MODEL:23; ::_thesis: verum
end;

theorem Th96: :: ZF_LANG1:96
for H being ZF-formula
for x, y being Variable
for M being non empty set st M |= H holds
M |= Ex (x,y,H)
proof
let H be ZF-formula; ::_thesis: for x, y being Variable
for M being non empty set st M |= H holds
M |= Ex (x,y,H)
let x, y be Variable; ::_thesis: for M being non empty set st M |= H holds
M |= Ex (x,y,H)
let M be non empty set ; ::_thesis: ( M |= H implies M |= Ex (x,y,H) )
 ( M |= H implies M |= Ex (y,H) ) by Th94;
hence  ( M |= H implies M |= Ex (x,y,H) ) by Th94; ::_thesis: verum
end;

theorem :: ZF_LANG1:97
for H being ZF-formula
for x, y, z being Variable
for M being non empty set holds
( M |= H iff M |= All (x,y,z,H) )
proof
let H be ZF-formula; ::_thesis: for x, y, z being Variable
for M being non empty set holds
( M |= H iff M |= All (x,y,z,H) )
let x, y, z be Variable; ::_thesis: for M being non empty set holds
( M |= H iff M |= All (x,y,z,H) )
let M be non empty set ; ::_thesis: ( M |= H iff M |= All (x,y,z,H) )
 ( M |= H iff M |= All (y,z,H) ) by Th95;
hence  ( M |= H iff M |= All (x,y,z,H) ) by ZF_MODEL:23; ::_thesis: verum
end;

theorem :: ZF_LANG1:98
for H being ZF-formula
for x, y, z being Variable
for M being non empty set st M |= H holds
M |= Ex (x,y,z,H)
proof
let H be ZF-formula; ::_thesis: for x, y, z being Variable
for M being non empty set st M |= H holds
M |= Ex (x,y,z,H)
let x, y, z be Variable; ::_thesis: for M being non empty set st M |= H holds
M |= Ex (x,y,z,H)
let M be non empty set ; ::_thesis: ( M |= H implies M |= Ex (x,y,z,H) )
 ( M |= H implies M |= Ex (y,z,H) ) by Th96;
hence  ( M |= H implies M |= Ex (x,y,z,H) ) by Th94; ::_thesis: verum
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) )
proof
let p, q be ZF-formula; ::_thesis: 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) )
let M be non empty set ; ::_thesis: for v being Function of VAR,M holds
( M,v |= (p <=> q) => (p => q) & M |= (p <=> q) => (p => q) )
let v be Function of VAR,M; ::_thesis: ( M,v |= (p <=> q) => (p => q) & M |= (p <=> q) => (p => q) )
A1: now__::_thesis:_for_v_being_Function_of_VAR,M_holds_M,v_|=_(p_<=>_q)_=>_(p_=>_q)
let v be Function of VAR,M; ::_thesis: M,v |= (p <=> q) => (p => q)
 ( M,v |= p <=> q implies M,v |= p => q ) by ZF_MODEL:15;
hence  M,v |= (p <=> q) => (p => q) by ZF_MODEL:18; ::_thesis: verum
end;
hence  M,v |= (p <=> q) => (p => q) ; ::_thesis: M |= (p <=> q) => (p => q)
let v be Function of VAR,M; :: according to ZF_MODEL:def_5 ::_thesis: M,v |= (p <=> q) => (p => q)
thus  M,v |= (p <=> q) => (p => q) by A1; ::_thesis: verum
end;

theorem :: ZF_LANG1:100
for p, q being ZF-formula
for M being non empty set
for v being Function of VAR,M holds
( M,v |= (p <=> q) => (q => p) & M |= (p <=> q) => (q => p) )
proof
let p, q be ZF-formula; ::_thesis: 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) )
let M be non empty set ; ::_thesis: for v being Function of VAR,M holds
( M,v |= (p <=> q) => (q => p) & M |= (p <=> q) => (q => p) )
let v be Function of VAR,M; ::_thesis: ( M,v |= (p <=> q) => (q => p) & M |= (p <=> q) => (q => p) )
A1: now__::_thesis:_for_v_being_Function_of_VAR,M_holds_M,v_|=_(p_<=>_q)_=>_(q_=>_p)
let v be Function of VAR,M; ::_thesis: M,v |= (p <=> q) => (q => p)
 ( M,v |= p <=> q implies M,v |= q => p ) by ZF_MODEL:15;
hence  M,v |= (p <=> q) => (q => p) by ZF_MODEL:18; ::_thesis: verum
end;
hence  M,v |= (p <=> q) => (q => p) ; ::_thesis: M |= (p <=> q) => (q => p)
let v be Function of VAR,M; :: according to ZF_MODEL:def_5 ::_thesis: M,v |= (p <=> q) => (q => p)
thus  M,v |= (p <=> q) => (q => p) by A1; ::_thesis: verum
end;

theorem Th101: :: ZF_LANG1:101
for p, q, r being ZF-formula
for M being non empty set holds M |= (p => q) => ((q => r) => (p => r))
proof
let p, q, r be ZF-formula; ::_thesis: for M being non empty set holds M |= (p => q) => ((q => r) => (p => r))
let M be non empty set ; ::_thesis: M |= (p => q) => ((q => r) => (p => r))
let v be Function of VAR,M; :: according to ZF_MODEL:def_5 ::_thesis: M,v |= (p => q) => ((q => r) => (p => r))
now__::_thesis:_(_M,v_|=_p_=>_q_implies_M,v_|=_(q_=>_r)_=>_(p_=>_r)_)
assume A1: M,v |= p => q ; ::_thesis: M,v |= (q => r) => (p => r)
now__::_thesis:_(_M,v_|=_q_=>_r_implies_M,v_|=_p_=>_r_)
assume A2: M,v |= q => r ; ::_thesis: M,v |= p => r
now__::_thesis:_(_M,v_|=_p_implies_M,v_|=_r_)
assume  M,v |= p ; ::_thesis: M,v |= r
then  M,v |= q by A1, ZF_MODEL:18;
hence  M,v |= r by A2, ZF_MODEL:18; ::_thesis: verum
end;
hence  M,v |= p => r by ZF_MODEL:18; ::_thesis: verum
end;
hence  M,v |= (q => r) => (p => r) by ZF_MODEL:18; ::_thesis: verum
end;
hence  M,v |= (p => q) => ((q => r) => (p => r)) by ZF_MODEL:18; ::_thesis: verum
end;

theorem Th102: :: ZF_LANG1:102
for p, q, r being ZF-formula
for M being non empty set
for v being Function of VAR,M st M,v |= p => q & M,v |= q => r holds
M,v |= p => r
proof
let p, q, r be ZF-formula; ::_thesis: 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
let M be non empty set ; ::_thesis: for v being Function of VAR,M st M,v |= p => q & M,v |= q => r holds
M,v |= p => r
let v be Function of VAR,M; ::_thesis: ( M,v |= p => q & M,v |= q => r implies M,v |= p => r )
assume that
A1: M,v |= p => q and
A2: M,v |= q => r ; ::_thesis: M,v |= p => r
 M |= (p => q) => ((q => r) => (p => r)) by Th101;
then  M,v |= (p => q) => ((q => r) => (p => r)) by ZF_MODEL:def_5;
then  M,v |= (q => r) => (p => r) by A1, ZF_MODEL:18;
hence  M,v |= p => r by A2, ZF_MODEL:18; ::_thesis: verum
end;

theorem :: ZF_LANG1:103
for p, q, r being ZF-formula
for M being non empty set st M |= p => q & M |= q => r holds
M |= p => r
proof
let p, q, r be ZF-formula; ::_thesis: for M being non empty set st M |= p => q & M |= q => r holds
M |= p => r
let M be non empty set ; ::_thesis: ( M |= p => q & M |= q => r implies M |= p => r )
assume A1: ( M |= p => q & M |= q => r ) ; ::_thesis: M |= p => r
let v be Function of VAR,M; :: according to ZF_MODEL:def_5 ::_thesis: M,v |= p => r
 ( M,v |= p => q & M,v |= q => r ) by A1, ZF_MODEL:def_5;
hence  M,v |= p => r by Th102; ::_thesis: verum
end;

theorem :: ZF_LANG1:104
for p, q, r being ZF-formula
for M being non empty set
for v being Function of VAR,M holds
( M,v |= ((p => q) '&' (q => r)) => (p => r) & M |= ((p => q) '&' (q => r)) => (p => r) )
proof
let p, q, r be ZF-formula; ::_thesis: 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) )
let M be non empty set ; ::_thesis: for v being Function of VAR,M holds
( M,v |= ((p => q) '&' (q => r)) => (p => r) & M |= ((p => q) '&' (q => r)) => (p => r) )
let v be Function of VAR,M; ::_thesis: ( M,v |= ((p => q) '&' (q => r)) => (p => r) & M |= ((p => q) '&' (q => r)) => (p => r) )
now__::_thesis:_for_v_being_Function_of_VAR,M_holds_M,v_|=_((p_=>_q)_'&'_(q_=>_r))_=>_(p_=>_r)
let v be Function of VAR,M; ::_thesis: M,v |= ((p => q) '&' (q => r)) => (p => r)
now__::_thesis:_(_M,v_|=_(p_=>_q)_'&'_(q_=>_r)_implies_M,v_|=_p_=>_r_)
assume  M,v |= (p => q) '&' (q => r) ; ::_thesis: M,v |= p => r
then  ( M,v |= p => q & M,v |= q => r ) by ZF_MODEL:15;
hence  M,v |= p => r by Th102; ::_thesis: verum
end;
hence  M,v |= ((p => q) '&' (q => r)) => (p => r) by ZF_MODEL:18; ::_thesis: verum
end;
hence  ( M,v |= ((p => q) '&' (q => r)) => (p => r) & M |= ((p => q) '&' (q => r)) => (p => r) ) by ZF_MODEL:def_5; ::_thesis: verum
end;

theorem :: ZF_LANG1:105
for p, q being ZF-formula
for M being non empty set
for v being Function of VAR,M holds
( M,v |= p => (q => p) & M |= p => (q => p) )
proof
let p, q be ZF-formula; ::_thesis: for M being non empty set
for v being Function of VAR,M holds
( M,v |= p => (q => p) & M |= p => (q => p) )
let M be non empty set ; ::_thesis: for v being Function of VAR,M holds
( M,v |= p => (q => p) & M |= p => (q => p) )
let v be Function of VAR,M; ::_thesis: ( M,v |= p => (q => p) & M |= p => (q => p) )
now__::_thesis:_for_v_being_Function_of_VAR,M_holds_M,v_|=_p_=>_(q_=>_p)
let v be Function of VAR,M; ::_thesis: M,v |= p => (q => p)
 ( M,v |= p implies M,v |= q => p ) by ZF_MODEL:18;
hence  M,v |= p => (q => p) by ZF_MODEL:18; ::_thesis: verum
end;
hence  ( M,v |= p => (q => p) & M |= p => (q => p) ) by ZF_MODEL:def_5; ::_thesis: verum
end;

theorem :: ZF_LANG1:106
for p, q, r being ZF-formula
for M being non empty set
for v being Function of VAR,M holds
( M,v |= (p => (q => r)) => ((p => q) => (p => r)) & M |= (p => (q => r)) => ((p => q) => (p => r)) )
proof
let p, q, r be ZF-formula; ::_thesis: 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)) )
let M be non empty set ; ::_thesis: 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)) )
let v be Function of VAR,M; ::_thesis: ( M,v |= (p => (q => r)) => ((p => q) => (p => r)) & M |= (p => (q => r)) => ((p => q) => (p => r)) )
now__::_thesis:_for_v_being_Function_of_VAR,M_holds_M,v_|=_(p_=>_(q_=>_r))_=>_((p_=>_q)_=>_(p_=>_r))
let v be Function of VAR,M; ::_thesis: M,v |= (p => (q => r)) => ((p => q) => (p => r))
now__::_thesis:_(_M,v_|=_p_=>_(q_=>_r)_implies_M,v_|=_(p_=>_q)_=>_(p_=>_r)_)
assume A1: M,v |= p => (q => r) ; ::_thesis: M,v |= (p => q) => (p => r)
now__::_thesis:_(_M,v_|=_p_=>_q_implies_M,v_|=_p_=>_r_)
assume  M,v |= p => q ; ::_thesis: M,v |= p => r
then A2: ( M,v |= p implies ( M,v |= q => r & M,v |= q ) ) by A1, ZF_MODEL:18;
 ( M,v |= q & M,v |= q => r implies M,v |= r ) by ZF_MODEL:18;
hence  M,v |= p => r by A2, ZF_MODEL:18; ::_thesis: verum
end;
hence  M,v |= (p => q) => (p => r) by ZF_MODEL:18; ::_thesis: verum
end;
hence  M,v |= (p => (q => r)) => ((p => q) => (p => r)) by ZF_MODEL:18; ::_thesis: verum
end;
hence  ( M,v |= (p => (q => r)) => ((p => q) => (p => r)) & M |= (p => (q => r)) => ((p => q) => (p => r)) ) by ZF_MODEL:def_5; ::_thesis: verum
end;

theorem :: ZF_LANG1:107
for p, q being ZF-formula
for M being non empty set
for v being Function of VAR,M holds
( M,v |= (p '&' q) => p & M |= (p '&' q) => p )
proof
let p, q be ZF-formula; ::_thesis: for M being non empty set
for v being Function of VAR,M holds
( M,v |= (p '&' q) => p & M |= (p '&' q) => p )
let M be non empty set ; ::_thesis: for v being Function of VAR,M holds
( M,v |= (p '&' q) => p & M |= (p '&' q) => p )
let v be Function of VAR,M; ::_thesis: ( M,v |= (p '&' q) => p & M |= (p '&' q) => p )
now__::_thesis:_for_v_being_Function_of_VAR,M_holds_M,v_|=_(p_'&'_q)_=>_p
let v be Function of VAR,M; ::_thesis: M,v |= (p '&' q) => p
 ( M,v |= p '&' q implies M,v |= p ) by ZF_MODEL:15;
hence  M,v |= (p '&' q) => p by ZF_MODEL:18; ::_thesis: verum
end;
hence  ( M,v |= (p '&' q) => p & M |= (p '&' q) => p ) by ZF_MODEL:def_5; ::_thesis: verum
end;

theorem :: ZF_LANG1:108
for p, q being ZF-formula
for M being non empty set
for v being Function of VAR,M holds
( M,v |= (p '&' q) => q & M |= (p '&' q) => q )
proof
let p, q be ZF-formula; ::_thesis: for M being non empty set
for v being Function of VAR,M holds
( M,v |= (p '&' q) => q & M |= (p '&' q) => q )
let M be non empty set ; ::_thesis: for v being Function of VAR,M holds
( M,v |= (p '&' q) => q & M |= (p '&' q) => q )
let v be Function of VAR,M; ::_thesis: ( M,v |= (p '&' q) => q & M |= (p '&' q) => q )
now__::_thesis:_for_v_being_Function_of_VAR,M_holds_M,v_|=_(p_'&'_q)_=>_q
let v be Function of VAR,M; ::_thesis: M,v |= (p '&' q) => q
 ( M,v |= p '&' q implies M,v |= q ) by ZF_MODEL:15;
hence  M,v |= (p '&' q) => q by ZF_MODEL:18; ::_thesis: verum
end;
hence  ( M,v |= (p '&' q) => q & M |= (p '&' q) => q ) by ZF_MODEL:def_5; ::_thesis: verum
end;

theorem :: ZF_LANG1:109
for p, q being ZF-formula
for M being non empty set
for v being Function of VAR,M holds
( M,v |= (p '&' q) => (q '&' p) & M |= (p '&' q) => (q '&' p) )
proof
let p, q be ZF-formula; ::_thesis: 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) )
let M be non empty set ; ::_thesis: for v being Function of VAR,M holds
( M,v |= (p '&' q) => (q '&' p) & M |= (p '&' q) => (q '&' p) )
let v be Function of VAR,M; ::_thesis: ( M,v |= (p '&' q) => (q '&' p) & M |= (p '&' q) => (q '&' p) )
now__::_thesis:_for_v_being_Function_of_VAR,M_holds_M,v_|=_(p_'&'_q)_=>_(q_'&'_p)
let v be Function of VAR,M; ::_thesis: M,v |= (p '&' q) => (q '&' p)
A1: ( M,v |= p & M,v |= q implies M,v |= q '&' p ) by ZF_MODEL:15;
 ( M,v |= p '&' q implies ( M,v |= p & M,v |= q ) ) by ZF_MODEL:15;
hence  M,v |= (p '&' q) => (q '&' p) by A1, ZF_MODEL:18; ::_thesis: verum
end;
hence  ( M,v |= (p '&' q) => (q '&' p) & M |= (p '&' q) => (q '&' p) ) by ZF_MODEL:def_5; ::_thesis: verum
end;

theorem :: ZF_LANG1:110
for p being ZF-formula
for M being non empty set
for v being Function of VAR,M holds
( M,v |= p => (p '&' p) & M |= p => (p '&' p) )
proof
let p be ZF-formula; ::_thesis: for M being non empty set
for v being Function of VAR,M holds
( M,v |= p => (p '&' p) & M |= p => (p '&' p) )
let M be non empty set ; ::_thesis: for v being Function of VAR,M holds
( M,v |= p => (p '&' p) & M |= p => (p '&' p) )
let v be Function of VAR,M; ::_thesis: ( M,v |= p => (p '&' p) & M |= p => (p '&' p) )
now__::_thesis:_for_v_being_Function_of_VAR,M_holds_M,v_|=_p_=>_(p_'&'_p)
let v be Function of VAR,M; ::_thesis: M,v |= p => (p '&' p)
 ( M,v |= p implies M,v |= p '&' p ) by ZF_MODEL:15;
hence  M,v |= p => (p '&' p) by ZF_MODEL:18; ::_thesis: verum
end;
hence  ( M,v |= p => (p '&' p) & M |= p => (p '&' p) ) by ZF_MODEL:def_5; ::_thesis: verum
end;

theorem :: ZF_LANG1:111
for p, q, r being ZF-formula
for M being non empty set
for v being Function of VAR,M holds
( M,v |= (p => q) => ((p => r) => (p => (q '&' r))) & M |= (p => q) => ((p => r) => (p => (q '&' r))) )
proof
let p, q, r be ZF-formula; ::_thesis: 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))) )
let M be non empty set ; ::_thesis: 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))) )
let v be Function of VAR,M; ::_thesis: ( M,v |= (p => q) => ((p => r) => (p => (q '&' r))) & M |= (p => q) => ((p => r) => (p => (q '&' r))) )
now__::_thesis:_for_v_being_Function_of_VAR,M_holds_M,v_|=_(p_=>_q)_=>_((p_=>_r)_=>_(p_=>_(q_'&'_r)))
let v be Function of VAR,M; ::_thesis: M,v |= (p => q) => ((p => r) => (p => (q '&' r)))
now__::_thesis:_(_M,v_|=_p_=>_q_implies_M,v_|=_(p_=>_r)_=>_(p_=>_(q_'&'_r))_)
assume A1: M,v |= p => q ; ::_thesis: M,v |= (p => r) => (p => (q '&' r))
now__::_thesis:_(_M,v_|=_p_=>_r_implies_M,v_|=_p_=>_(q_'&'_r)_)
assume  M,v |= p => r ; ::_thesis: M,v |= p => (q '&' r)
then  ( M,v |= p implies ( M,v |= r & M,v |= q ) ) by A1, ZF_MODEL:18;
then  ( M,v |= p implies M,v |= q '&' r ) by ZF_MODEL:15;
hence  M,v |= p => (q '&' r) by ZF_MODEL:18; ::_thesis: verum
end;
hence  M,v |= (p => r) => (p => (q '&' r)) by ZF_MODEL:18; ::_thesis: verum
end;
hence  M,v |= (p => q) => ((p => r) => (p => (q '&' r))) by ZF_MODEL:18; ::_thesis: verum
end;
hence  ( M,v |= (p => q) => ((p => r) => (p => (q '&' r))) & M |= (p => q) => ((p => r) => (p => (q '&' r))) ) by ZF_MODEL:def_5; ::_thesis: verum
end;

theorem Th112: :: ZF_LANG1:112
for p, q being ZF-formula
for M being non empty set
for v being Function of VAR,M holds
( M,v |= p => (p 'or' q) & M |= p => (p 'or' q) )
proof
let p, q be ZF-formula; ::_thesis: 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) )
let M be non empty set ; ::_thesis: for v being Function of VAR,M holds
( M,v |= p => (p 'or' q) & M |= p => (p 'or' q) )
let v be Function of VAR,M; ::_thesis: ( M,v |= p => (p 'or' q) & M |= p => (p 'or' q) )
now__::_thesis:_for_v_being_Function_of_VAR,M_holds_M,v_|=_p_=>_(p_'or'_q)
let v be Function of VAR,M; ::_thesis: M,v |= p => (p 'or' q)
 ( M,v |= p implies M,v |= p 'or' q ) by ZF_MODEL:17;
hence  M,v |= p => (p 'or' q) by ZF_MODEL:18; ::_thesis: verum
end;
hence  ( M,v |= p => (p 'or' q) & M |= p => (p 'or' q) ) by ZF_MODEL:def_5; ::_thesis: verum
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) )
proof
let q, p be ZF-formula; ::_thesis: 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) )
let M be non empty set ; ::_thesis: for v being Function of VAR,M holds
( M,v |= q => (p 'or' q) & M |= q => (p 'or' q) )
let v be Function of VAR,M; ::_thesis: ( M,v |= q => (p 'or' q) & M |= q => (p 'or' q) )
now__::_thesis:_for_v_being_Function_of_VAR,M_holds_M,v_|=_q_=>_(p_'or'_q)
let v be Function of VAR,M; ::_thesis: M,v |= q => (p 'or' q)
 ( M,v |= q implies M,v |= p 'or' q ) by ZF_MODEL:17;
hence  M,v |= q => (p 'or' q) by ZF_MODEL:18; ::_thesis: verum
end;
hence  ( M,v |= q => (p 'or' q) & M |= q => (p 'or' q) ) by ZF_MODEL:def_5; ::_thesis: verum
end;

theorem :: ZF_LANG1:114
for p, q being ZF-formula
for M being non empty set
for v being Function of VAR,M holds
( M,v |= (p 'or' q) => (q 'or' p) & M |= (p 'or' q) => (q 'or' p) )
proof
let p, q be ZF-formula; ::_thesis: 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) )
let M be non empty set ; ::_thesis: for v being Function of VAR,M holds
( M,v |= (p 'or' q) => (q 'or' p) & M |= (p 'or' q) => (q 'or' p) )
let v be Function of VAR,M; ::_thesis: ( M,v |= (p 'or' q) => (q 'or' p) & M |= (p 'or' q) => (q 'or' p) )
now__::_thesis:_for_v_being_Function_of_VAR,M_holds_M,v_|=_(p_'or'_q)_=>_(q_'or'_p)
let v be Function of VAR,M; ::_thesis: M,v |= (p 'or' q) => (q 'or' p)
A1: ( ( M,v |= p or M,v |= q ) implies M,v |= q 'or' p ) by ZF_MODEL:17;
 ( not M,v |= p 'or' q or M,v |= p or M,v |= q ) by ZF_MODEL:17;
hence  M,v |= (p 'or' q) => (q 'or' p) by A1, ZF_MODEL:18; ::_thesis: verum
end;
hence  ( M,v |= (p 'or' q) => (q 'or' p) & M |= (p 'or' q) => (q 'or' p) ) by ZF_MODEL:def_5; ::_thesis: verum
end;

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

theorem :: ZF_LANG1:116
for p, 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
let p, r, q be ZF-formula; ::_thesis: 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)) )
let M be non empty set ; ::_thesis: 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)) )
let v be Function of VAR,M; ::_thesis: ( M,v |= (p => r) => ((q => r) => ((p 'or' q) => r)) & M |= (p => r) => ((q => r) => ((p 'or' q) => r)) )
now__::_thesis:_for_v_being_Function_of_VAR,M_holds_M,v_|=_(p_=>_r)_=>_((q_=>_r)_=>_((p_'or'_q)_=>_r))
let v be Function of VAR,M; ::_thesis: M,v |= (p => r) => ((q => r) => ((p 'or' q) => r))
now__::_thesis:_(_M,v_|=_p_=>_r_implies_M,v_|=_(q_=>_r)_=>_((p_'or'_q)_=>_r)_)
assume A1: M,v |= p => r ; ::_thesis: M,v |= (q => r) => ((p 'or' q) => r)
now__::_thesis:_(_M,v_|=_q_=>_r_implies_M,v_|=_(p_'or'_q)_=>_r_)
assume  M,v |= q => r ; ::_thesis: M,v |= (p 'or' q) => r
then  ( ( M,v |= p or M,v |= q ) implies M,v |= r ) by A1, ZF_MODEL:18;
then  ( M,v |= p 'or' q implies M,v |= r ) by ZF_MODEL:17;
hence  M,v |= (p 'or' q) => r by ZF_MODEL:18; ::_thesis: verum
end;
hence  M,v |= (q => r) => ((p 'or' q) => r) by ZF_MODEL:18; ::_thesis: verum
end;
hence  M,v |= (p => r) => ((q => r) => ((p 'or' q) => r)) by ZF_MODEL:18; ::_thesis: verum
end;
hence  ( M,v |= (p => r) => ((q => r) => ((p 'or' q) => r)) & M |= (p => r) => ((q => r) => ((p 'or' q) => r)) ) by ZF_MODEL:def_5; ::_thesis: verum
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) )
proof
let p, r, q be ZF-formula; ::_thesis: 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) )
let M be non empty set ; ::_thesis: 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) )
let v be Function of VAR,M; ::_thesis: ( M,v |= ((p => r) '&' (q => r)) => ((p 'or' q) => r) & M |= ((p => r) '&' (q => r)) => ((p 'or' q) => r) )
now__::_thesis:_for_v_being_Function_of_VAR,M_holds_M,v_|=_((p_=>_r)_'&'_(q_=>_r))_=>_((p_'or'_q)_=>_r)
let v be Function of VAR,M; ::_thesis: M,v |= ((p => r) '&' (q => r)) => ((p 'or' q) => r)
now__::_thesis:_(_M,v_|=_(p_=>_r)_'&'_(q_=>_r)_implies_M,v_|=_(p_'or'_q)_=>_r_)
assume  M,v |= (p => r) '&' (q => r) ; ::_thesis: M,v |= (p 'or' q) => r
then  ( M,v |= p => r & M,v |= q => r ) by ZF_MODEL:15;
then  ( ( M,v |= p or M,v |= q ) implies M,v |= r ) by ZF_MODEL:18;
then  ( M,v |= p 'or' q implies M,v |= r ) by ZF_MODEL:17;
hence  M,v |= (p 'or' q) => r by ZF_MODEL:18; ::_thesis: verum
end;
hence  M,v |= ((p => r) '&' (q => r)) => ((p 'or' q) => r) by ZF_MODEL:18; ::_thesis: verum
end;
hence  ( M,v |= ((p => r) '&' (q => r)) => ((p 'or' q) => r) & M |= ((p => r) '&' (q => r)) => ((p 'or' q) => r) ) by ZF_MODEL:def_5; ::_thesis: verum
end;

theorem :: ZF_LANG1:118
for p, q being ZF-formula
for M being non empty set
for v being Function of VAR,M holds
( M,v |= (p => ('not' q)) => (q => ('not' p)) & M |= (p => ('not' q)) => (q => ('not' p)) )
proof
let p, q be ZF-formula; ::_thesis: 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)) )
let M be non empty set ; ::_thesis: for v being Function of VAR,M holds
( M,v |= (p => ('not' q)) => (q => ('not' p)) & M |= (p => ('not' q)) => (q => ('not' p)) )
let v be Function of VAR,M; ::_thesis: ( M,v |= (p => ('not' q)) => (q => ('not' p)) & M |= (p => ('not' q)) => (q => ('not' p)) )
now__::_thesis:_for_v_being_Function_of_VAR,M_holds_M,v_|=_(p_=>_('not'_q))_=>_(q_=>_('not'_p))
let v be Function of VAR,M; ::_thesis: M,v |= (p => ('not' q)) => (q => ('not' p))
now__::_thesis:_(_M,v_|=_p_=>_('not'_q)_implies_M,v_|=_q_=>_('not'_p)_)
assume  M,v |= p => ('not' q) ; ::_thesis: M,v |= q => ('not' p)
then  ( M,v |= p implies M,v |= 'not' q ) by ZF_MODEL:18;
then  ( M,v |= q implies M,v |= 'not' p ) by ZF_MODEL:14;
hence  M,v |= q => ('not' p) by ZF_MODEL:18; ::_thesis: verum
end;
hence  M,v |= (p => ('not' q)) => (q => ('not' p)) by ZF_MODEL:18; ::_thesis: verum
end;
hence  ( M,v |= (p => ('not' q)) => (q => ('not' p)) & M |= (p => ('not' q)) => (q => ('not' p)) ) by ZF_MODEL:def_5; ::_thesis: verum
end;

theorem :: ZF_LANG1:119
for p, q being ZF-formula
for M being non empty set
for v being Function of VAR,M holds
( M,v |= ('not' p) => (p => q) & M |= ('not' p) => (p => q) )
proof
let p, q be ZF-formula; ::_thesis: 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) )
let M be non empty set ; ::_thesis: for v being Function of VAR,M holds
( M,v |= ('not' p) => (p => q) & M |= ('not' p) => (p => q) )
let v be Function of VAR,M; ::_thesis: ( M,v |= ('not' p) => (p => q) & M |= ('not' p) => (p => q) )
now__::_thesis:_for_v_being_Function_of_VAR,M_holds_M,v_|=_('not'_p)_=>_(p_=>_q)
let v be Function of VAR,M; ::_thesis: M,v |= ('not' p) => (p => q)
now__::_thesis:_(_M,v_|=_'not'_p_implies_M,v_|=_p_=>_q_)
assume  M,v |= 'not' p ; ::_thesis: M,v |= p => q
then  not M,v |= p by ZF_MODEL:14;
hence  M,v |= p => q by ZF_MODEL:18; ::_thesis: verum
end;
hence  M,v |= ('not' p) => (p => q) by ZF_MODEL:18; ::_thesis: verum
end;
hence  ( M,v |= ('not' p) => (p => q) & M |= ('not' p) => (p => q) ) by ZF_MODEL:def_5; ::_thesis: verum
end;

theorem :: ZF_LANG1:120
for p, q being ZF-formula
for M being non empty set
for v being Function of VAR,M holds
( M,v |= ((p => q) '&' (p => ('not' q))) => ('not' p) & M |= ((p => q) '&' (p => ('not' q))) => ('not' p) )
proof
let p, q be ZF-formula; ::_thesis: 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) )
let M be non empty set ; ::_thesis: 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) )
let v be Function of VAR,M; ::_thesis: ( M,v |= ((p => q) '&' (p => ('not' q))) => ('not' p) & M |= ((p => q) '&' (p => ('not' q))) => ('not' p) )
now__::_thesis:_for_v_being_Function_of_VAR,M_holds_M,v_|=_((p_=>_q)_'&'_(p_=>_('not'_q)))_=>_('not'_p)
let v be Function of VAR,M; ::_thesis: M,v |= ((p => q) '&' (p => ('not' q))) => ('not' p)
now__::_thesis:_(_M,v_|=_(p_=>_q)_'&'_(p_=>_('not'_q))_implies_M,v_|=_'not'_p_)
assume  M,v |= (p => q) '&' (p => ('not' q)) ; ::_thesis: M,v |= 'not' p
then  ( M,v |= p => q & M,v |= p => ('not' q) ) by ZF_MODEL:15;
then  ( M,v |= p implies ( M,v |= q & M,v |= 'not' q ) ) by ZF_MODEL:18;
hence  M,v |= 'not' p by ZF_MODEL:14; ::_thesis: verum
end;
hence  M,v |= ((p => q) '&' (p => ('not' q))) => ('not' p) by ZF_MODEL:18; ::_thesis: verum
end;
hence  ( M,v |= ((p => q) '&' (p => ('not' q))) => ('not' p) & M |= ((p => q) '&' (p => ('not' q))) => ('not' p) ) by ZF_MODEL:def_5; ::_thesis: verum
end;

theorem :: ZF_LANG1:121
for p, q being ZF-formula
for M being non empty set st M |= p => q & M |= p holds
M |= q
proof
let p, q be ZF-formula; ::_thesis: for M being non empty set st M |= p => q & M |= p holds
M |= q
let M be non empty set ; ::_thesis: ( M |= p => q & M |= p implies M |= q )
assume A1: ( M |= p => q & M |= p ) ; ::_thesis: M |= q
let v be Function of VAR,M; :: according to ZF_MODEL:def_5 ::_thesis: M,v |= q
 ( M,v |= p => q & M,v |= p ) by A1, ZF_MODEL:def_5;
hence  M,v |= q by ZF_MODEL:18; ::_thesis: verum
end;

theorem :: ZF_LANG1:122
for p, q being ZF-formula
for M being non empty set
for v being Function of VAR,M holds
( M,v |= ('not' (p '&' q)) => (('not' p) 'or' ('not' q)) & M |= ('not' (p '&' q)) => (('not' p) 'or' ('not' q)) )
proof
let p, q be ZF-formula; ::_thesis: 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)) )
let M be non empty set ; ::_thesis: 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)) )
let v be Function of VAR,M; ::_thesis: ( M,v |= ('not' (p '&' q)) => (('not' p) 'or' ('not' q)) & M |= ('not' (p '&' q)) => (('not' p) 'or' ('not' q)) )
now__::_thesis:_for_v_being_Function_of_VAR,M_holds_M,v_|=_('not'_(p_'&'_q))_=>_(('not'_p)_'or'_('not'_q))
let v be Function of VAR,M; ::_thesis: M,v |= ('not' (p '&' q)) => (('not' p) 'or' ('not' q))
now__::_thesis:_(_M,v_|=_'not'_(p_'&'_q)_implies_M,v_|=_('not'_p)_'or'_('not'_q)_)
assume  M,v |= 'not' (p '&' q) ; ::_thesis: M,v |= ('not' p) 'or' ('not' q)
then  not M,v |= p '&' q by ZF_MODEL:14;
then  ( not M,v |= p or not M,v |= q ) by ZF_MODEL:15;
then  ( M,v |= 'not' p or M,v |= 'not' q ) by ZF_MODEL:14;
hence  M,v |= ('not' p) 'or' ('not' q) by ZF_MODEL:17; ::_thesis: verum
end;
hence  M,v |= ('not' (p '&' q)) => (('not' p) 'or' ('not' q)) by ZF_MODEL:18; ::_thesis: verum
end;
hence  ( M,v |= ('not' (p '&' q)) => (('not' p) 'or' ('not' q)) & M |= ('not' (p '&' q)) => (('not' p) 'or' ('not' q)) ) by ZF_MODEL:def_5; ::_thesis: verum
end;

theorem :: ZF_LANG1:123
for p, q being ZF-formula
for M being non empty set
for v being Function of VAR,M holds
( M,v |= (('not' p) 'or' ('not' q)) => ('not' (p '&' q)) & M |= (('not' p) 'or' ('not' q)) => ('not' (p '&' q)) )
proof
let p, q be ZF-formula; ::_thesis: 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)) )
let M be non empty set ; ::_thesis: 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)) )
let v be Function of VAR,M; ::_thesis: ( M,v |= (('not' p) 'or' ('not' q)) => ('not' (p '&' q)) & M |= (('not' p) 'or' ('not' q)) => ('not' (p '&' q)) )
now__::_thesis:_for_v_being_Function_of_VAR,M_holds_M,v_|=_(('not'_p)_'or'_('not'_q))_=>_('not'_(p_'&'_q))
let v be Function of VAR,M; ::_thesis: M,v |= (('not' p) 'or' ('not' q)) => ('not' (p '&' q))
now__::_thesis:_(_M,v_|=_('not'_p)_'or'_('not'_q)_implies_M,v_|=_'not'_(p_'&'_q)_)
assume  M,v |= ('not' p) 'or' ('not' q) ; ::_thesis: M,v |= 'not' (p '&' q)
then  ( M,v |= 'not' p or M,v |= 'not' q ) by ZF_MODEL:17;
then  ( not M,v |= p or not M,v |= q ) by ZF_MODEL:14;
then  not M,v |= p '&' q by ZF_MODEL:15;
hence  M,v |= 'not' (p '&' q) by ZF_MODEL:14; ::_thesis: verum
end;
hence  M,v |= (('not' p) 'or' ('not' q)) => ('not' (p '&' q)) by ZF_MODEL:18; ::_thesis: verum
end;
hence  ( M,v |= (('not' p) 'or' ('not' q)) => ('not' (p '&' q)) & M |= (('not' p) 'or' ('not' q)) => ('not' (p '&' q)) ) by ZF_MODEL:def_5; ::_thesis: verum
end;

theorem :: ZF_LANG1:124
for p, q being ZF-formula
for M being non empty set
for v being Function of VAR,M holds
( M,v |= ('not' (p 'or' q)) => (('not' p) '&' ('not' q)) & M |= ('not' (p 'or' q)) => (('not' p) '&' ('not' q)) )
proof
let p, q be ZF-formula; ::_thesis: 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)) )
let M be non empty set ; ::_thesis: 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)) )
let v be Function of VAR,M; ::_thesis: ( M,v |= ('not' (p 'or' q)) => (('not' p) '&' ('not' q)) & M |= ('not' (p 'or' q)) => (('not' p) '&' ('not' q)) )
now__::_thesis:_for_v_being_Function_of_VAR,M_holds_M,v_|=_('not'_(p_'or'_q))_=>_(('not'_p)_'&'_('not'_q))
let v be Function of VAR,M; ::_thesis: M,v |= ('not' (p 'or' q)) => (('not' p) '&' ('not' q))
now__::_thesis:_(_M,v_|=_'not'_(p_'or'_q)_implies_M,v_|=_('not'_p)_'&'_('not'_q)_)
assume  M,v |= 'not' (p 'or' q) ; ::_thesis: M,v |= ('not' p) '&' ('not' q)
then A1: not M,v |= p 'or' q by ZF_MODEL:14;
then  not M,v |= q by ZF_MODEL:17;
then A2: M,v |= 'not' q by ZF_MODEL:14;
 not M,v |= p by A1, ZF_MODEL:17;
then  M,v |= 'not' p by ZF_MODEL:14;
hence  M,v |= ('not' p) '&' ('not' q) by A2, ZF_MODEL:15; ::_thesis: verum
end;
hence  M,v |= ('not' (p 'or' q)) => (('not' p) '&' ('not' q)) by ZF_MODEL:18; ::_thesis: verum
end;
hence  ( M,v |= ('not' (p 'or' q)) => (('not' p) '&' ('not' q)) & M |= ('not' (p 'or' q)) => (('not' p) '&' ('not' q)) ) by ZF_MODEL:def_5; ::_thesis: verum
end;

theorem :: ZF_LANG1:125
for p, q being ZF-formula
for M being non empty set
for v being Function of VAR,M holds
( M,v |= (('not' p) '&' ('not' q)) => ('not' (p 'or' q)) & M |= (('not' p) '&' ('not' q)) => ('not' (p 'or' q)) )
proof
let p, q be ZF-formula; ::_thesis: 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)) )
let M be non empty set ; ::_thesis: 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)) )
let v be Function of VAR,M; ::_thesis: ( M,v |= (('not' p) '&' ('not' q)) => ('not' (p 'or' q)) & M |= (('not' p) '&' ('not' q)) => ('not' (p 'or' q)) )
now__::_thesis:_for_v_being_Function_of_VAR,M_holds_M,v_|=_(('not'_p)_'&'_('not'_q))_=>_('not'_(p_'or'_q))
let v be Function of VAR,M; ::_thesis: M,v |= (('not' p) '&' ('not' q)) => ('not' (p 'or' q))
now__::_thesis:_(_M,v_|=_('not'_p)_'&'_('not'_q)_implies_M,v_|=_'not'_(p_'or'_q)_)
assume A1: M,v |= ('not' p) '&' ('not' q) ; ::_thesis: M,v |= 'not' (p 'or' q)
then  M,v |= 'not' q by ZF_MODEL:15;
then A2: not M,v |= q by ZF_MODEL:14;
 M,v |= 'not' p by A1, ZF_MODEL:15;
then  not M,v |= p by ZF_MODEL:14;
then  not M,v |= p 'or' q by A2, ZF_MODEL:17;
hence  M,v |= 'not' (p 'or' q) by ZF_MODEL:14; ::_thesis: verum
end;
hence  M,v |= (('not' p) '&' ('not' q)) => ('not' (p 'or' q)) by ZF_MODEL:18; ::_thesis: verum
end;
hence  ( M,v |= (('not' p) '&' ('not' q)) => ('not' (p 'or' q)) & M |= (('not' p) '&' ('not' q)) => ('not' (p 'or' q)) ) by ZF_MODEL:def_5; ::_thesis: verum
end;

theorem :: ZF_LANG1:126
for H being ZF-formula
for x being Variable
for M being non empty set holds M |= (All (x,H)) => H
proof
let H be ZF-formula; ::_thesis: for x being Variable
for M being non empty set holds M |= (All (x,H)) => H
let x be Variable; ::_thesis: for M being non empty set holds M |= (All (x,H)) => H
let M be non empty set ; ::_thesis: M |= (All (x,H)) => H
let v be Function of VAR,M; :: according to ZF_MODEL:def_5 ::_thesis: M,v |= (All (x,H)) => H
 ( M,v |= All (x,H) implies M,v / (x,(v . x)) |= H ) by Th71;
then  ( M,v |= All (x,H) implies M,v |= H ) by FUNCT_7:35;
hence  M,v |= (All (x,H)) => H by ZF_MODEL:18; ::_thesis: verum
end;

theorem :: ZF_LANG1:127
for H being ZF-formula
for x being Variable
for M being non empty set holds M |= H => (Ex (x,H))
proof
let H be ZF-formula; ::_thesis: for x being Variable
for M being non empty set holds M |= H => (Ex (x,H))
let x be Variable; ::_thesis: for M being non empty set holds M |= H => (Ex (x,H))
let M be non empty set ; ::_thesis: M |= H => (Ex (x,H))
let v be Function of VAR,M; :: according to ZF_MODEL:def_5 ::_thesis: M,v |= H => (Ex (x,H))
 ( M,v / (x,(v . x)) |= H implies M,v |= Ex (x,H) ) by Th73;
then  ( M,v |= H implies M,v |= Ex (x,H) ) by FUNCT_7:35;
hence  M,v |= H => (Ex (x,H)) by ZF_MODEL:18; ::_thesis: verum
end;

theorem Th128: :: ZF_LANG1:128
for H1, H2 being ZF-formula
for x being Variable
for M being non empty set st not x in Free H1 holds
M |= (All (x,(H1 => H2))) => (H1 => (All (x,H2)))
proof
let H1, H2 be ZF-formula; ::_thesis: 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)))
let x be Variable; ::_thesis: for M being non empty set st not x in Free H1 holds
M |= (All (x,(H1 => H2))) => (H1 => (All (x,H2)))
let M be non empty set ; ::_thesis: ( not x in Free H1 implies M |= (All (x,(H1 => H2))) => (H1 => (All (x,H2))) )
assume A1: not x in Free H1 ; ::_thesis: M |= (All (x,(H1 => H2))) => (H1 => (All (x,H2)))
let v be Function of VAR,M; :: according to ZF_MODEL:def_5 ::_thesis: M,v |= (All (x,(H1 => H2))) => (H1 => (All (x,H2)))
now__::_thesis:_(_M,v_|=_All_(x,(H1_=>_H2))_implies_M,v_|=_H1_=>_(All_(x,H2))_)
assume A2: M,v |= All (x,(H1 => H2)) ; ::_thesis: M,v |= H1 => (All (x,H2))
now__::_thesis:_(_M,v_|=_H1_implies_M,v_|=_All_(x,H2)_)
assume A3: M,v |= H1 ; ::_thesis: M,v |= All (x,H2)
now__::_thesis:_for_m_being_Element_of_M_holds_M,v_/_(x,m)_|=_H2
let m be Element of M; ::_thesis: M,v / (x,m) |= H2
 M,v |= All (x,H1) by A1, A3, ZFMODEL1:10;
then A4: M,v / (x,m) |= H1 by Th71;
 M,v / (x,m) |= H1 => H2 by A2, Th71;
hence  M,v / (x,m) |= H2 by A4, ZF_MODEL:18; ::_thesis: verum
end;
hence  M,v |= All (x,H2) by Th71; ::_thesis: verum
end;
hence  M,v |= H1 => (All (x,H2)) by ZF_MODEL:18; ::_thesis: verum
end;
hence  M,v |= (All (x,(H1 => H2))) => (H1 => (All (x,H2))) by ZF_MODEL:18; ::_thesis: verum
end;

theorem :: ZF_LANG1:129
for H1, H2 being ZF-formula
for x being Variable
for M being non empty set st not x in Free H1 & M |= H1 => H2 holds
M |= H1 => (All (x,H2))
proof
let H1, H2 be ZF-formula; ::_thesis: 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))
let x be Variable; ::_thesis: for M being non empty set st not x in Free H1 & M |= H1 => H2 holds
M |= H1 => (All (x,H2))
let M be non empty set ; ::_thesis: ( not x in Free H1 & M |= H1 => H2 implies M |= H1 => (All (x,H2)) )
assume that
A1: not x in Free H1 and
A2: for v being Function of VAR,M holds M,v |= H1 => H2 ; :: according to ZF_MODEL:def_5 ::_thesis: M |= H1 => (All (x,H2))
let v be Function of VAR,M; :: according to ZF_MODEL:def_5 ::_thesis: M,v |= H1 => (All (x,H2))
 M |= (All (x,(H1 => H2))) => (H1 => (All (x,H2))) by A1, Th128;
then A3: M,v |= (All (x,(H1 => H2))) => (H1 => (All (x,H2))) by ZF_MODEL:def_5;
 for m being Element of M holds M,v / (x,m) |= H1 => H2 by A2;
then  M,v |= All (x,(H1 => H2)) by Th71;
hence  M,v |= H1 => (All (x,H2)) by A3, ZF_MODEL:18; ::_thesis: verum
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)
proof
let H2, H1 be ZF-formula; ::_thesis: 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)
let x be Variable; ::_thesis: for M being non empty set st not x in Free H2 holds
M |= (All (x,(H1 => H2))) => ((Ex (x,H1)) => H2)
let M be non empty set ; ::_thesis: ( not x in Free H2 implies M |= (All (x,(H1 => H2))) => ((Ex (x,H1)) => H2) )
assume A1: not x in Free H2 ; ::_thesis: M |= (All (x,(H1 => H2))) => ((Ex (x,H1)) => H2)
let v be Function of VAR,M; :: according to ZF_MODEL:def_5 ::_thesis: M,v |= (All (x,(H1 => H2))) => ((Ex (x,H1)) => H2)
now__::_thesis:_(_M,v_|=_All_(x,(H1_=>_H2))_implies_M,v_|=_(Ex_(x,H1))_=>_H2_)
assume A2: M,v |= All (x,(H1 => H2)) ; ::_thesis: M,v |= (Ex (x,H1)) => H2
now__::_thesis:_(_M,v_|=_Ex_(x,H1)_implies_M,v_|=_H2_)
assume  M,v |= Ex (x,H1) ; ::_thesis: M,v |= H2
then consider m being Element of M such that
A3: M,v / (x,m) |= H1 by Th73;
 M,v / (x,m) |= H1 => H2 by A2, Th71;
then  M,v / (x,m) |= H2 by A3, ZF_MODEL:18;
then  M,v / (x,m) |= All (x,H2) by A1, ZFMODEL1:10;
then  M,v |= All (x,H2) by Th72;
then  M,v / (x,(v . x)) |= H2 by Th71;
hence  M,v |= H2 by FUNCT_7:35; ::_thesis: verum
end;
hence  M,v |= (Ex (x,H1)) => H2 by ZF_MODEL:18; ::_thesis: verum
end;
hence  M,v |= (All (x,(H1 => H2))) => ((Ex (x,H1)) => H2) by ZF_MODEL:18; ::_thesis: verum
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
proof
let H2, H1 be ZF-formula; ::_thesis: 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
let x be Variable; ::_thesis: for M being non empty set st not x in Free H2 & M |= H1 => H2 holds
M |= (Ex (x,H1)) => H2
let M be non empty set ; ::_thesis: ( not x in Free H2 & M |= H1 => H2 implies M |= (Ex (x,H1)) => H2 )
assume that
A1: not x in Free H2 and
A2: for v being Function of VAR,M holds M,v |= H1 => H2 ; :: according to ZF_MODEL:def_5 ::_thesis: M |= (Ex (x,H1)) => H2
let v be Function of VAR,M; :: according to ZF_MODEL:def_5 ::_thesis: M,v |= (Ex (x,H1)) => H2
 M |= (All (x,(H1 => H2))) => ((Ex (x,H1)) => H2) by A1, Th130;
then A3: M,v |= (All (x,(H1 => H2))) => ((Ex (x,H1)) => H2) by ZF_MODEL:def_5;
 for m being Element of M holds M,v / (x,m) |= H1 => H2 by A2;
then  M,v |= All (x,(H1 => H2)) by Th71;
hence  M,v |= (Ex (x,H1)) => H2 by A3, ZF_MODEL:18; ::_thesis: verum
end;

theorem :: ZF_LANG1:132
for H1, H2 being ZF-formula
for x being Variable
for M being non empty set st M |= H1 => (All (x,H2)) holds
M |= H1 => H2
proof
let H1, H2 be ZF-formula; ::_thesis: for x being Variable
for M being non empty set st M |= H1 => (All (x,H2)) holds
M |= H1 => H2
let x be Variable; ::_thesis: for M being non empty set st M |= H1 => (All (x,H2)) holds
M |= H1 => H2
let M be non empty set ; ::_thesis: ( M |= H1 => (All (x,H2)) implies M |= H1 => H2 )
assume A1: for v being Function of VAR,M holds M,v |= H1 => (All (x,H2)) ; :: according to ZF_MODEL:def_5 ::_thesis: M |= H1 => H2
let v be Function of VAR,M; :: according to ZF_MODEL:def_5 ::_thesis: M,v |= H1 => H2
A2: M,v |= H1 => (All (x,H2)) by A1;
now__::_thesis:_(_M,v_|=_H1_implies_M,v_|=_H2_)
assume  M,v |= H1 ; ::_thesis: M,v |= H2
then  M,v |= All (x,H2) by A2, ZF_MODEL:18;
then  M,v / (x,(v . x)) |= H2 by Th71;
hence  M,v |= H2 by FUNCT_7:35; ::_thesis: verum
end;
hence  M,v |= H1 => H2 by ZF_MODEL:18; ::_thesis: verum
end;

theorem :: ZF_LANG1:133
for H1, H2 being ZF-formula
for x being Variable
for M being non empty set st M |= (Ex (x,H1)) => H2 holds
M |= H1 => H2
proof
let H1, H2 be ZF-formula; ::_thesis: for x being Variable
for M being non empty set st M |= (Ex (x,H1)) => H2 holds
M |= H1 => H2
let x be Variable; ::_thesis: for M being non empty set st M |= (Ex (x,H1)) => H2 holds
M |= H1 => H2
let M be non empty set ; ::_thesis: ( M |= (Ex (x,H1)) => H2 implies M |= H1 => H2 )
assume A1: for v being Function of VAR,M holds M,v |= (Ex (x,H1)) => H2 ; :: according to ZF_MODEL:def_5 ::_thesis: M |= H1 => H2
let v be Function of VAR,M; :: according to ZF_MODEL:def_5 ::_thesis: M,v |= H1 => H2
A2: M,v |= (Ex (x,H1)) => H2 by A1;
now__::_thesis:_(_M,v_|=_H1_implies_M,v_|=_H2_)
assume  M,v |= H1 ; ::_thesis: M,v |= H2
then  M,v / (x,(v . x)) |= H1 by FUNCT_7:35;
then  M,v |= Ex (x,H1) by Th73;
hence  M,v |= H2 by A2, ZF_MODEL:18; ::_thesis: verum
end;
hence  M,v |= H1 => H2 by ZF_MODEL:18; ::_thesis: verum
end;

theorem :: ZF_LANG1:134
WFF c= bool [:NAT,NAT:]
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in WFF or a in bool [:NAT,NAT:] )
assume  a in WFF ; ::_thesis: a in bool [:NAT,NAT:]
then reconsider H = a as ZF-formula by ZF_LANG:4;
 H c= [:NAT,NAT:] ;
hence  a in bool [:NAT,NAT:] ; ::_thesis: verum
end;

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

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

theorem Th135: :: ZF_LANG1:135
for x being Variable holds
( x <> 0 & x <> 1 & x <> 2 & x <> 3 & x <> 4 )
proof
let x be Variable; ::_thesis: ( x <> 0 & x <> 1 & x <> 2 & x <> 3 & x <> 4 )
 x in VAR ;
then A1: ex i being Element of NAT st
( x = i & 5 <= i ) ;
assume  ( x = 0 or x = 1 or x = 2 or x = 3 or x = 4 ) ; ::_thesis: contradiction
hence  contradiction by A1; ::_thesis: verum
end;

theorem Th136: :: ZF_LANG1:136
for x being Variable holds not x in {0,1,2,3,4}
proof
let x be Variable; ::_thesis: not x in {0,1,2,3,4}
assume  x in {0,1,2,3,4} ; ::_thesis: contradiction
then  x in {0,1} \/ {2,3,4} by ENUMSET1:8;
then  ( x in {0,1} or x in {2,3,4} ) by XBOOLE_0:def_3;
then A1: ( x = 0 or x = 1 or x = 2 or x = 3 or x = 4 ) by ENUMSET1:def_1, TARSKI:def_2;
 x in VAR ;
then  ex i being Element of NAT st
( x = i & 5 <= i ) ;
hence  contradiction by A1; ::_thesis: verum
end;

theorem Th137: :: ZF_LANG1:137
for H being ZF-formula
for a being set st a in variables_in H holds
( a <> 0 & a <> 1 & a <> 2 & a <> 3 & a <> 4 )
proof
let H be ZF-formula; ::_thesis: for a being set st a in variables_in H holds
( a <> 0 & a <> 1 & a <> 2 & a <> 3 & a <> 4 )
let a be set ; ::_thesis: ( a in variables_in H implies ( a <> 0 & a <> 1 & a <> 2 & a <> 3 & a <> 4 ) )
assume  a in variables_in H ; ::_thesis: ( a <> 0 & a <> 1 & a <> 2 & a <> 3 & a <> 4 )
then  not a in {0,1,2,3,4} by XBOOLE_0:def_5;
then  not a in {0,1} \/ {2,3,4} by ENUMSET1:8;
then  ( not a in {0,1} & not a in {2,3,4} ) by XBOOLE_0:def_3;
hence  ( a <> 0 & a <> 1 & a <> 2 & a <> 3 & a <> 4 ) by ENUMSET1:def_1, TARSKI:def_2; ::_thesis: verum
end;

theorem Th138: :: ZF_LANG1:138
for x, y being Variable holds variables_in (x '=' y) = {x,y}
proof
let x, y be Variable; ::_thesis: variables_in (x '=' y) = {x,y}
A1: rng (x '=' y) = (rng (<*0*> ^ <*x*>)) \/ (rng <*y*>) by FINSEQ_1:31
.= ((rng <*0*>) \/ (rng <*x*>)) \/ (rng <*y*>) by FINSEQ_1:31
.= ({0} \/ (rng <*x*>)) \/ (rng <*y*>) by FINSEQ_1:39
.= ({0} \/ {x}) \/ (rng <*y*>) by FINSEQ_1:39
.= ({0} \/ {x}) \/ {y} by FINSEQ_1:39
.= {0} \/ ({x} \/ {y}) by XBOOLE_1:4
.= {0} \/ {x,y} by ENUMSET1:1 ;
thus  variables_in (x '=' y) c= {x,y} :: according to XBOOLE_0:def_10 ::_thesis: {x,y} c= variables_in (x '=' y)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in variables_in (x '=' y) or a in {x,y} )
assume A2: a in variables_in (x '=' y) ; ::_thesis: a in {x,y}
then  a <> 0 by Th137;
then  not a in {0} by TARSKI:def_1;
hence  a in {x,y} by A1, A2, XBOOLE_0:def_3; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {x,y} or a in variables_in (x '=' y) )
assume A3: a in {x,y} ; ::_thesis: a in variables_in (x '=' y)
then  ( a = x or a = y ) by TARSKI:def_2;
then A4: not a in {0,1,2,3,4} by Th136;
 a in {0} \/ {x,y} by A3, XBOOLE_0:def_3;
hence  a in variables_in (x '=' y) by A1, A4, XBOOLE_0:def_5; ::_thesis: verum
end;

theorem Th139: :: ZF_LANG1:139
for x, y being Variable holds variables_in (x 'in' y) = {x,y}
proof
let x, y be Variable; ::_thesis: variables_in (x 'in' y) = {x,y}
A1: rng (x 'in' y) = (rng (<*1*> ^ <*x*>)) \/ (rng <*y*>) by FINSEQ_1:31
.= ((rng <*1*>) \/ (rng <*x*>)) \/ (rng <*y*>) by FINSEQ_1:31
.= ({1} \/ (rng <*x*>)) \/ (rng <*y*>) by FINSEQ_1:39
.= ({1} \/ {x}) \/ (rng <*y*>) by FINSEQ_1:39
.= ({1} \/ {x}) \/ {y} by FINSEQ_1:39
.= {1} \/ ({x} \/ {y}) by XBOOLE_1:4
.= {1} \/ {x,y} by ENUMSET1:1 ;
thus  variables_in (x 'in' y) c= {x,y} :: according to XBOOLE_0:def_10 ::_thesis: {x,y} c= variables_in (x 'in' y)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in variables_in (x 'in' y) or a in {x,y} )
assume A2: a in variables_in (x 'in' y) ; ::_thesis: a in {x,y}
then  a <> 1 by Th137;
then  not a in {1} by TARSKI:def_1;
hence  a in {x,y} by A1, A2, XBOOLE_0:def_3; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {x,y} or a in variables_in (x 'in' y) )
assume A3: a in {x,y} ; ::_thesis: a in variables_in (x 'in' y)
then  ( a = x or a = y ) by TARSKI:def_2;
then A4: not a in {0,1,2,3,4} by Th136;
 a in {1} \/ {x,y} by A3, XBOOLE_0:def_3;
hence  a in variables_in (x 'in' y) by A1, A4, XBOOLE_0:def_5; ::_thesis: verum
end;

theorem Th140: :: ZF_LANG1:140
for H being ZF-formula holds variables_in ('not' H) = variables_in H
proof
let H be ZF-formula; ::_thesis: variables_in ('not' H) = variables_in H
A1: rng ('not' H) = (rng <*2*>) \/ (rng H) by FINSEQ_1:31
.= {2} \/ (rng H) by FINSEQ_1:39 ;
thus  variables_in ('not' H) c= variables_in H :: according to XBOOLE_0:def_10 ::_thesis: variables_in H c= variables_in ('not' H)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in variables_in ('not' H) or a in variables_in H )
assume A2: a in variables_in ('not' H) ; ::_thesis: a in variables_in H
then  a <> 2 by Th137;
then  not a in {2} by TARSKI:def_1;
then A3: a in rng H by A1, A2, XBOOLE_0:def_3;
 not a in {0,1,2,3,4} by A2, XBOOLE_0:def_5;
hence  a in variables_in H by A3, XBOOLE_0:def_5; ::_thesis: verum
end;
thus  variables_in H c= variables_in ('not' H) by A1, XBOOLE_1:7, XBOOLE_1:33; ::_thesis: verum
end;

theorem Th141: :: ZF_LANG1:141
for H1, H2 being ZF-formula holds variables_in (H1 '&' H2) = (variables_in H1) \/ (variables_in H2)
proof
let H1, H2 be ZF-formula; ::_thesis: variables_in (H1 '&' H2) = (variables_in H1) \/ (variables_in H2)
A1: (variables_in H1) \/ (variables_in H2) = ((rng H1) \/ (rng H2)) \ {0,1,2,3,4} by XBOOLE_1:42;
A2: rng (H1 '&' H2) = (rng (<*3*> ^ H1)) \/ (rng H2) by FINSEQ_1:31
.= ((rng <*3*>) \/ (rng H1)) \/ (rng H2) by FINSEQ_1:31
.= ({3} \/ (rng H1)) \/ (rng H2) by FINSEQ_1:39
.= {3} \/ ((rng H1) \/ (rng H2)) by XBOOLE_1:4 ;
thus  variables_in (H1 '&' H2) c= (variables_in H1) \/ (variables_in H2) :: according to XBOOLE_0:def_10 ::_thesis: (variables_in H1) \/ (variables_in H2) c= variables_in (H1 '&' H2)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in variables_in (H1 '&' H2) or a in (variables_in H1) \/ (variables_in H2) )
assume A3: a in variables_in (H1 '&' H2) ; ::_thesis: a in (variables_in H1) \/ (variables_in H2)
then  a <> 3 by Th137;
then  not a in {3} by TARSKI:def_1;
then A4: a in (rng H1) \/ (rng H2) by A2, A3, XBOOLE_0:def_3;
 not a in {0,1,2,3,4} by A3, XBOOLE_0:def_5;
hence  a in (variables_in H1) \/ (variables_in H2) by A1, A4, XBOOLE_0:def_5; ::_thesis: verum
end;
thus  (variables_in H1) \/ (variables_in H2) c= variables_in (H1 '&' H2) by A2, A1, XBOOLE_1:7, XBOOLE_1:33; ::_thesis: verum
end;

theorem Th142: :: ZF_LANG1:142
for H being ZF-formula
for x being Variable holds variables_in (All (x,H)) = (variables_in H) \/ {x}
proof
let H be ZF-formula; ::_thesis: for x being Variable holds variables_in (All (x,H)) = (variables_in H) \/ {x}
let x be Variable; ::_thesis: variables_in (All (x,H)) = (variables_in H) \/ {x}
A1: rng (All (x,H)) = (rng (<*4*> ^ <*x*>)) \/ (rng H) by FINSEQ_1:31
.= ((rng <*4*>) \/ (rng <*x*>)) \/ (rng H) by FINSEQ_1:31
.= ({4} \/ (rng <*x*>)) \/ (rng H) by FINSEQ_1:39
.= ({4} \/ {x}) \/ (rng H) by FINSEQ_1:39
.= {4} \/ ({x} \/ (rng H)) by XBOOLE_1:4 ;
thus  variables_in (All (x,H)) c= (variables_in H) \/ {x} :: according to XBOOLE_0:def_10 ::_thesis: (variables_in H) \/ {x} c= variables_in (All (x,H))
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in variables_in (All (x,H)) or a in (variables_in H) \/ {x} )
assume A2: a in variables_in (All (x,H)) ; ::_thesis: a in (variables_in H) \/ {x}
then  a <> 4 by Th137;
then  not a in {4} by TARSKI:def_1;
then  a in {x} \/ (rng H) by A1, A2, XBOOLE_0:def_3;
then A3: ( a in {x} or a in rng H ) by XBOOLE_0:def_3;
 not a in {0,1,2,3,4} by A2, XBOOLE_0:def_5;
then  ( a in rng H implies a in variables_in H ) by XBOOLE_0:def_5;
hence  a in (variables_in H) \/ {x} by A3, XBOOLE_0:def_3; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (variables_in H) \/ {x} or a in variables_in (All (x,H)) )
assume  a in (variables_in H) \/ {x} ; ::_thesis: a in variables_in (All (x,H))
then A4: ( a in variables_in H or a in {x} ) by XBOOLE_0:def_3;
then  a in {x} \/ (rng H) by XBOOLE_0:def_3;
then A5: a in {4} \/ ({x} \/ (rng H)) by XBOOLE_0:def_3;
 ( ( a in rng H & not a in {0,1,2,3,4} ) or ( a in {x} & x = a ) ) by A4, TARSKI:def_1, XBOOLE_0:def_5;
then  not a in {0,1,2,3,4} by Th136;
hence  a in variables_in (All (x,H)) by A1, A5, XBOOLE_0:def_5; ::_thesis: verum
end;

theorem :: ZF_LANG1:143
for H1, H2 being ZF-formula holds variables_in (H1 'or' H2) = (variables_in H1) \/ (variables_in H2)
proof
let H1, H2 be ZF-formula; ::_thesis: variables_in (H1 'or' H2) = (variables_in H1) \/ (variables_in H2)
thus  variables_in (H1 'or' H2) = variables_in (('not' H1) '&' ('not' H2)) by Th140
.= (variables_in ('not' H1)) \/ (variables_in ('not' H2)) by Th141
.= (variables_in H1) \/ (variables_in ('not' H2)) by Th140
.= (variables_in H1) \/ (variables_in H2) by Th140 ; ::_thesis: verum
end;

theorem Th144: :: ZF_LANG1:144
for H1, H2 being ZF-formula holds variables_in (H1 => H2) = (variables_in H1) \/ (variables_in H2)
proof
let H1, H2 be ZF-formula; ::_thesis: variables_in (H1 => H2) = (variables_in H1) \/ (variables_in H2)
thus  variables_in (H1 => H2) = variables_in (H1 '&' ('not' H2)) by Th140
.= (variables_in H1) \/ (variables_in ('not' H2)) by Th141
.= (variables_in H1) \/ (variables_in H2) by Th140 ; ::_thesis: verum
end;

theorem :: ZF_LANG1:145
for H1, H2 being ZF-formula holds variables_in (H1 <=> H2) = (variables_in H1) \/ (variables_in H2)
proof
let H1, H2 be ZF-formula; ::_thesis: variables_in (H1 <=> H2) = (variables_in H1) \/ (variables_in H2)
thus  variables_in (H1 <=> H2) = (variables_in (H1 => H2)) \/ (variables_in (H2 => H1)) by Th141
.= ((variables_in H1) \/ (variables_in H2)) \/ (variables_in (H2 => H1)) by Th144
.= ((variables_in H1) \/ (variables_in H2)) \/ ((variables_in H1) \/ (variables_in H2)) by Th144
.= (variables_in H1) \/ (variables_in H2) ; ::_thesis: verum
end;

theorem Th146: :: ZF_LANG1:146
for H being ZF-formula
for x being Variable holds variables_in (Ex (x,H)) = (variables_in H) \/ {x}
proof
let H be ZF-formula; ::_thesis: for x being Variable holds variables_in (Ex (x,H)) = (variables_in H) \/ {x}
let x be Variable; ::_thesis: variables_in (Ex (x,H)) = (variables_in H) \/ {x}
thus  variables_in (Ex (x,H)) = variables_in (All (x,('not' H))) by Th140
.= (variables_in ('not' H)) \/ {x} by Th142
.= (variables_in H) \/ {x} by Th140 ; ::_thesis: verum
end;

theorem Th147: :: ZF_LANG1:147
for H being ZF-formula
for x, y being Variable holds variables_in (All (x,y,H)) = (variables_in H) \/ {x,y}
proof
let H be ZF-formula; ::_thesis: for x, y being Variable holds variables_in (All (x,y,H)) = (variables_in H) \/ {x,y}
let x, y be Variable; ::_thesis: variables_in (All (x,y,H)) = (variables_in H) \/ {x,y}
thus  variables_in (All (x,y,H)) = (variables_in (All (y,H))) \/ {x} by Th142
.= ((variables_in H) \/ {y}) \/ {x} by Th142
.= (variables_in H) \/ ({y} \/ {x}) by XBOOLE_1:4
.= (variables_in H) \/ {x,y} by ENUMSET1:1 ; ::_thesis: verum
end;

theorem Th148: :: ZF_LANG1:148
for H being ZF-formula
for x, y being Variable holds variables_in (Ex (x,y,H)) = (variables_in H) \/ {x,y}
proof
let H be ZF-formula; ::_thesis: for x, y being Variable holds variables_in (Ex (x,y,H)) = (variables_in H) \/ {x,y}
let x, y be Variable; ::_thesis: variables_in (Ex (x,y,H)) = (variables_in H) \/ {x,y}
thus  variables_in (Ex (x,y,H)) = (variables_in (Ex (y,H))) \/ {x} by Th146
.= ((variables_in H) \/ {y}) \/ {x} by Th146
.= (variables_in H) \/ ({y} \/ {x}) by XBOOLE_1:4
.= (variables_in H) \/ {x,y} by ENUMSET1:1 ; ::_thesis: verum
end;

theorem :: ZF_LANG1:149
for H being ZF-formula
for x, y, z being Variable holds variables_in (All (x,y,z,H)) = (variables_in H) \/ {x,y,z}
proof
let H be ZF-formula; ::_thesis: for x, y, z being Variable holds variables_in (All (x,y,z,H)) = (variables_in H) \/ {x,y,z}
let x, y, z be Variable; ::_thesis: variables_in (All (x,y,z,H)) = (variables_in H) \/ {x,y,z}
thus  variables_in (All (x,y,z,H)) = (variables_in (All (y,z,H))) \/ {x} by Th142
.= ((variables_in H) \/ {y,z}) \/ {x} by Th147
.= (variables_in H) \/ ({y,z} \/ {x}) by XBOOLE_1:4
.= (variables_in H) \/ {y,z,x} by ENUMSET1:3
.= (variables_in H) \/ {x,y,z} by ENUMSET1:59 ; ::_thesis: verum
end;

theorem :: ZF_LANG1:150
for H being ZF-formula
for x, y, z being Variable holds variables_in (Ex (x,y,z,H)) = (variables_in H) \/ {x,y,z}
proof
let H be ZF-formula; ::_thesis: for x, y, z being Variable holds variables_in (Ex (x,y,z,H)) = (variables_in H) \/ {x,y,z}
let x, y, z be Variable; ::_thesis: variables_in (Ex (x,y,z,H)) = (variables_in H) \/ {x,y,z}
thus  variables_in (Ex (x,y,z,H)) = (variables_in (Ex (y,z,H))) \/ {x} by Th146
.= ((variables_in H) \/ {y,z}) \/ {x} by Th148
.= (variables_in H) \/ ({y,z} \/ {x}) by XBOOLE_1:4
.= (variables_in H) \/ {y,z,x} by ENUMSET1:3
.= (variables_in H) \/ {x,y,z} by ENUMSET1:59 ; ::_thesis: verum
end;

theorem :: ZF_LANG1:151
for H being ZF-formula holds Free H c= variables_in H
proof
let H be ZF-formula; ::_thesis: Free H c= variables_in H
defpred S1[ ZF-formula] means  Free $1 c= variables_in $1;
A1: for H1 being ZF-formula st S1[H1] holds
S1[ 'not' H1]
proof
let H1 be ZF-formula; ::_thesis: ( S1[H1] implies S1[ 'not' H1] )
assume  Free H1 c= variables_in H1 ; ::_thesis: S1[ 'not' H1]
then  Free ('not' H1) c= variables_in H1 by Th60;
hence  S1[ 'not' H1] by Th140; ::_thesis: verum
end;
A2: for H1, H2 being ZF-formula st S1[H1] & S1[H2] holds
S1[H1 '&' H2]
proof
let H1, H2 be ZF-formula; ::_thesis: ( S1[H1] & S1[H2] implies S1[H1 '&' H2] )
assume  ( Free H1 c= variables_in H1 & Free H2 c= variables_in H2 ) ; ::_thesis: S1[H1 '&' H2]
then  (Free H1) \/ (Free H2) c= (variables_in H1) \/ (variables_in H2) by XBOOLE_1:13;
then  Free (H1 '&' H2) c= (variables_in H1) \/ (variables_in H2) by Th61;
hence  S1[H1 '&' H2] by Th141; ::_thesis: verum
end;
A3: for H1 being ZF-formula
for x being Variable st S1[H1] holds
S1[ All (x,H1)]
proof
let H1 be ZF-formula; ::_thesis: for x being Variable st S1[H1] holds
S1[ All (x,H1)]
let x be Variable; ::_thesis: ( S1[H1] implies S1[ All (x,H1)] )
 (Free H1) \ {x} c= Free H1 by XBOOLE_1:36;
then A4: Free (All (x,H1)) c= Free H1 by Th62;
 variables_in H1 c= (variables_in H1) \/ {x} by XBOOLE_1:7;
then A5: variables_in H1 c= variables_in (All (x,H1)) by Th142;
assume  Free H1 c= variables_in H1 ; ::_thesis: S1[ All (x,H1)]
then  Free H1 c= variables_in (All (x,H1)) by A5, XBOOLE_1:1;
hence  S1[ All (x,H1)] by A4, XBOOLE_1:1; ::_thesis: verum
end;
A6: for x, y being Variable holds
( S1[x '=' y] & S1[x 'in' y] )
proof
let x, y be Variable; ::_thesis: ( S1[x '=' y] & S1[x 'in' y] )
 ( variables_in (x '=' y) = {x,y} & variables_in (x 'in' y) = {x,y} ) by Th138, Th139;
hence  ( S1[x '=' y] & S1[x 'in' y] ) by Th58, Th59; ::_thesis: verum
end;
 for H being ZF-formula holds S1[H] from ZF_LANG1:sch_1(A6, A1, A2, A3);
hence  Free H c= variables_in H ; ::_thesis: verum
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
defpred S1[ ZF-formula] means  variables_in $1 <> {} ;
A1: for H1, H2 being ZF-formula st S1[H1] & S1[H2] holds
S1[H1 '&' H2]
proof
let H1, H2 be ZF-formula; ::_thesis: ( S1[H1] & S1[H2] implies S1[H1 '&' H2] )
 variables_in (H1 '&' H2) = (variables_in H1) \/ (variables_in H2) by Th141;
hence  ( S1[H1] & S1[H2] implies S1[H1 '&' H2] ) ; ::_thesis: verum
end;
A2: for H being ZF-formula
for x being Variable st S1[H] holds
S1[ All (x,H)]
proof
let H be ZF-formula; ::_thesis: for x being Variable st S1[H] holds
S1[ All (x,H)]
let x be Variable; ::_thesis: ( S1[H] implies S1[ All (x,H)] )
 variables_in (All (x,H)) = (variables_in H) \/ {x} by Th142;
hence  ( S1[H] implies S1[ All (x,H)] ) ; ::_thesis: verum
end;
A3: for x, y being Variable holds
( S1[x '=' y] & S1[x 'in' y] )
proof
let x, y be Variable; ::_thesis: ( S1[x '=' y] & S1[x 'in' y] )
 variables_in (x '=' y) = {x,y} by Th138;
hence  ( S1[x '=' y] & S1[x 'in' y] ) by Th139; ::_thesis: verum
end;
A4: for H being ZF-formula st S1[H] holds
S1[ 'not' H] by Th140;
 for H being ZF-formula holds S1[H] from ZF_LANG1:sch_1(A3, A4, A1, A2);
then reconsider D = variables_in H as non empty set ;
 D c= VAR
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in D or a in VAR )
A5: rng H c= NAT by FINSEQ_1:def_4;
A6: 0 + 1 = 1 ;
assume A7: a in D ; ::_thesis: a in VAR
then  a in rng H ;
then reconsider i = a as Element of NAT by A5;
 a <> 0 by A7, Th137;
then A8: 1 <= i by A6, NAT_1:13;
A9: 3 + 1 = 4 ;
A10: 2 + 1 = 3 ;
A11: 1 + 1 = 2 ;
 a <> 1 by A7, Th137;
then  1 < i by A8, XXREAL_0:1;
then A12: 2 <= i by A11, NAT_1:13;
 a <> 2 by A7, Th137;
then  2 < i by A12, XXREAL_0:1;
then A13: 3 <= i by A10, NAT_1:13;
 a <> 3 by A7, Th137;
then  3 < i by A13, XXREAL_0:1;
then A14: 4 <= i by A9, NAT_1:13;
 a <> 4 by A7, Th137;
then A15: 4 < i by A14, XXREAL_0:1;
 4 + 1 = 5 ;
then  5 <= i by A15, NAT_1:13;
hence  a in VAR ; ::_thesis: verum
end;
hence  variables_in H is non empty Subset of VAR ; ::_thesis: verum
end;
end;

definition
let H be ZF-formula;
let x, y be Variable;
funcH / (x,y) ->  Function means :Def3: :: ZF_LANG1:def 3
( dom it = dom H & ( 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 b1 being Function st
( dom b1 = dom H & ( for a being set st a in dom H holds
( ( H . a = x implies b1 . a = y ) & ( H . a <> x implies b1 . a = H . a ) ) ) )
proof
deffunc H1( set ) ->  set = H . $1;
deffunc H2( set ) ->  Variable = y;
set A = dom H;
defpred S1[ set ] means H . $1 = x;
thus  ex f being Function st
( dom f = dom H & ( for a being set st a in dom H holds
( ( S1[a] implies f . a = H2(a) ) & ( not S1[a] implies f . a = H1(a) ) ) ) ) from PARTFUN1:sch_1(); ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function st dom b1 = dom H & ( for a being set st a in dom H holds
( ( H . a = x implies b1 . a = y ) & ( H . a <> x implies b1 . a = H . a ) ) ) & dom b2 = dom H & ( for a being set st a in dom H holds
( ( H . a = x implies b2 . a = y ) & ( H . a <> x implies b2 . a = H . a ) ) ) holds
b1 = b2
proof
let f1, f2 be Function; ::_thesis: ( dom f1 = dom H & ( for a being set st a in dom H holds
( ( H . a = x implies f1 . a = y ) & ( H . a <> x implies f1 . a = H . a ) ) ) & dom f2 = dom H & ( for a being set st a in dom H holds
( ( H . a = x implies f2 . a = y ) & ( H . a <> x implies f2 . a = H . a ) ) ) implies f1 = f2 )
assume that
A1: dom f1 = dom H and
A2: for a being set st a in dom H holds
( ( H . a = x implies f1 . a = y ) & ( H . a <> x implies f1 . a = H . a ) ) and
A3: dom f2 = dom H and
A4: for a being set st a in dom H holds
( ( H . a = x implies f2 . a = y ) & ( H . a <> x implies f2 . a = H . a ) ) ; ::_thesis: f1 = f2
now__::_thesis:_for_a_being_set_st_a_in_dom_H_holds_
f1_._a_=_f2_._a
let a be set ; ::_thesis: ( a in dom H implies f1 . a = f2 . a )
assume A5: a in dom H ; ::_thesis: f1 . a = f2 . a
then A6: ( H . a <> x implies f1 . a = H . a ) by A2;
 ( H . a = x implies f1 . a = y ) by A2, A5;
hence  f1 . a = f2 . a by A4, A5, A6; ::_thesis: verum
end;
hence  f1 = f2 by A1, A3, FUNCT_1:2; ::_thesis: verum
end;
end;

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

theorem Th152: :: ZF_LANG1:152
for x1, x2, y1, y2, z1, z2 being Variable holds
( (x1 '=' x2) / (y1,y2) = z1 '=' z2 iff ( ( x1 <> y1 & x2 <> y1 & z1 = x1 & z2 = x2 ) or ( x1 = y1 & x2 <> y1 & z1 = y2 & z2 = x2 ) or ( x1 <> y1 & x2 = y1 & z1 = x1 & z2 = y2 ) or ( x1 = y1 & x2 = y1 & z1 = y2 & z2 = y2 ) ) )
proof
let x1, x2, y1, y2, z1, z2 be Variable; ::_thesis: ( (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 ) ) )
set H = x1 '=' x2;
set Hz = z1 '=' z2;
set f = (x1 '=' x2) / (y1,y2);
A1: ( (x1 '=' x2) . 1 = 0 & y1 <> 0 ) by Th135, ZF_LANG:15;
 x1 '=' x2 is being_equality by ZF_LANG:5;
then A2: x1 '=' x2 is atomic by ZF_LANG:def_15;
then A3: len (x1 '=' x2) = 3 by ZF_LANG:11;
then A4: dom (x1 '=' x2) = {1,2,3} by FINSEQ_1:def_3, FINSEQ_3:1;
 z1 '=' z2 is being_equality by ZF_LANG:5;
then A5: z1 '=' z2 is atomic by ZF_LANG:def_15;
then  len (z1 '=' z2) = 3 by ZF_LANG:11;
then A6: dom (z1 '=' z2) = Seg 3 by FINSEQ_1:def_3;
 Var1 (z1 '=' z2) = z1 by Th1;
then A7: (z1 '=' z2) . 2 = z1 by A5, ZF_LANG:35;
 Var2 (z1 '=' z2) = z2 by Th1;
then A8: (z1 '=' z2) . 3 = z2 by A5, ZF_LANG:35;
A9: Var2 (x1 '=' x2) = x2 by Th1;
then A10: (x1 '=' x2) . 3 = x2 by A2, ZF_LANG:35;
A11: Var1 (x1 '=' x2) = x1 by Th1;
then A12: (x1 '=' x2) . 2 = x1 by A2, ZF_LANG:35;
thus  ( not (x1 '=' x2) / (y1,y2) = z1 '=' z2 or ( 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 ) ) ::_thesis: ( ( ( 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 ) ) implies (x1 '=' x2) / (y1,y2) = z1 '=' z2 )
proof
assume A13: (x1 '=' x2) / (y1,y2) = z1 '=' z2 ; ::_thesis: ( ( 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 ) )
percases ( ( x1 <> y1 & x2 <> y1 ) or ( x1 = y1 & x2 <> y1 ) or ( x1 <> y1 & x2 = y1 ) or ( x1 = y1 & x2 = y1 ) ) ;
caseA14: ( x1 <> y1 & x2 <> y1 ) ; ::_thesis: ( z1 = x1 & z2 = x2 )
 ( 2 in dom (x1 '=' x2) & 3 in dom (x1 '=' x2) ) by A4, ENUMSET1:def_1;
hence  ( z1 = x1 & z2 = x2 ) by A12, A10, A7, A8, A13, A14, Def3; ::_thesis: verum
end;
caseA15: ( x1 = y1 & x2 <> y1 ) ; ::_thesis: ( z1 = y2 & z2 = x2 )
A16: ( 2 in dom (x1 '=' x2) & 3 in dom (x1 '=' x2) ) by A4, ENUMSET1:def_1;
 (x1 '=' x2) . 2 = y1 by A2, A11, A15, ZF_LANG:35;
hence  ( z1 = y2 & z2 = x2 ) by A10, A7, A8, A13, A15, A16, Def3; ::_thesis: verum
end;
caseA17: ( x1 <> y1 & x2 = y1 ) ; ::_thesis: ( z1 = x1 & z2 = y2 )
A18: ( 2 in dom (x1 '=' x2) & 3 in dom (x1 '=' x2) ) by A4, ENUMSET1:def_1;
 (x1 '=' x2) . 3 = y1 by A2, A9, A17, ZF_LANG:35;
hence  ( z1 = x1 & z2 = y2 ) by A12, A7, A8, A13, A17, A18, Def3; ::_thesis: verum
end;
caseA19: ( x1 = y1 & x2 = y1 ) ; ::_thesis: ( z1 = y2 & z2 = y2 )
A20: ( 2 in dom (x1 '=' x2) & 3 in dom (x1 '=' x2) ) by A4, ENUMSET1:def_1;
 ( (x1 '=' x2) . 2 = y1 & (x1 '=' x2) . 3 = y1 ) by A2, A11, A9, A19, ZF_LANG:35;
hence  ( z1 = y2 & z2 = y2 ) by A7, A8, A13, A20, Def3; ::_thesis: verum
end;
end;
end;
A21: dom (x1 '=' x2) = Seg 3 by A3, FINSEQ_1:def_3;
A22: dom ((x1 '=' x2) / (y1,y2)) = dom (x1 '=' x2) by Def3;
A23: now__::_thesis:_(_x1_<>_y1_&_x2_<>_y1_&_z1_=_x1_&_z2_=_x2_implies_(x1_'='_x2)_/_(y1,y2)_=_z1_'='_z2_)
assume A24: ( x1 <> y1 & x2 <> y1 & z1 = x1 & z2 = x2 ) ; ::_thesis: (x1 '=' x2) / (y1,y2) = z1 '=' z2
now__::_thesis:_for_a_being_set_st_a_in_dom_(x1_'='_x2)_holds_
(z1_'='_z2)_._a_=_((x1_'='_x2)_/_(y1,y2))_._a
let a be set ; ::_thesis: ( a in dom (x1 '=' x2) implies (z1 '=' z2) . a = ((x1 '=' x2) / (y1,y2)) . a )
assume A25: a in dom (x1 '=' x2) ; ::_thesis: (z1 '=' z2) . a = ((x1 '=' x2) / (y1,y2)) . a
then  ( a = 1 or a = 2 or a = 3 ) by A4, ENUMSET1:def_1;
hence  (z1 '=' z2) . a = ((x1 '=' x2) / (y1,y2)) . a by A12, A10, A1, A24, A25, Def3; ::_thesis: verum
end;
hence  (x1 '=' x2) / (y1,y2) = z1 '=' z2 by A22, A21, A6, FUNCT_1:2; ::_thesis: verum
end;
A26: (z1 '=' z2) . 1 = 0 by ZF_LANG:15;
A27: now__::_thesis:_(_x1_<>_y1_&_x2_=_y1_&_z1_=_x1_&_z2_=_y2_implies_(x1_'='_x2)_/_(y1,y2)_=_z1_'='_z2_)
assume A28: ( x1 <> y1 & x2 = y1 & z1 = x1 & z2 = y2 ) ; ::_thesis: (x1 '=' x2) / (y1,y2) = z1 '=' z2
now__::_thesis:_for_a_being_set_st_a_in_dom_(x1_'='_x2)_holds_
(z1_'='_z2)_._a_=_((x1_'='_x2)_/_(y1,y2))_._a
let a be set ; ::_thesis: ( a in dom (x1 '=' x2) implies (z1 '=' z2) . a = ((x1 '=' x2) / (y1,y2)) . a )
assume A29: a in dom (x1 '=' x2) ; ::_thesis: (z1 '=' z2) . a = ((x1 '=' x2) / (y1,y2)) . a
then  ( a = 1 or a = 2 or a = 3 ) by A4, ENUMSET1:def_1;
hence  (z1 '=' z2) . a = ((x1 '=' x2) / (y1,y2)) . a by A12, A10, A26, A7, A8, A1, A28, A29, Def3; ::_thesis: verum
end;
hence  (x1 '=' x2) / (y1,y2) = z1 '=' z2 by A22, A21, A6, FUNCT_1:2; ::_thesis: verum
end;
A30: now__::_thesis:_(_x1_=_y1_&_x2_=_y1_&_z1_=_y2_&_z2_=_y2_implies_(x1_'='_x2)_/_(y1,y2)_=_z1_'='_z2_)
assume A31: ( x1 = y1 & x2 = y1 & z1 = y2 & z2 = y2 ) ; ::_thesis: (x1 '=' x2) / (y1,y2) = z1 '=' z2
now__::_thesis:_for_a_being_set_st_a_in_dom_(x1_'='_x2)_holds_
(z1_'='_z2)_._a_=_((x1_'='_x2)_/_(y1,y2))_._a
let a be set ; ::_thesis: ( a in dom (x1 '=' x2) implies (z1 '=' z2) . a = ((x1 '=' x2) / (y1,y2)) . a )
assume A32: a in dom (x1 '=' x2) ; ::_thesis: (z1 '=' z2) . a = ((x1 '=' x2) / (y1,y2)) . a
then  ( a = 1 or a = 2 or a = 3 ) by A4, ENUMSET1:def_1;
hence  (z1 '=' z2) . a = ((x1 '=' x2) / (y1,y2)) . a by A12, A10, A26, A7, A8, A1, A31, A32, Def3; ::_thesis: verum
end;
hence  (x1 '=' x2) / (y1,y2) = z1 '=' z2 by A22, A21, A6, FUNCT_1:2; ::_thesis: verum
end;
now__::_thesis:_(_x1_=_y1_&_x2_<>_y1_&_z1_=_y2_&_z2_=_x2_implies_(x1_'='_x2)_/_(y1,y2)_=_z1_'='_z2_)
assume A33: ( x1 = y1 & x2 <> y1 & z1 = y2 & z2 = x2 ) ; ::_thesis: (x1 '=' x2) / (y1,y2) = z1 '=' z2
now__::_thesis:_for_a_being_set_st_a_in_dom_(x1_'='_x2)_holds_
(z1_'='_z2)_._a_=_((x1_'='_x2)_/_(y1,y2))_._a
let a be set ; ::_thesis: ( a in dom (x1 '=' x2) implies (z1 '=' z2) . a = ((x1 '=' x2) / (y1,y2)) . a )
assume A34: a in dom (x1 '=' x2) ; ::_thesis: (z1 '=' z2) . a = ((x1 '=' x2) / (y1,y2)) . a
then  ( a = 1 or a = 2 or a = 3 ) by A4, ENUMSET1:def_1;
hence  (z1 '=' z2) . a = ((x1 '=' x2) / (y1,y2)) . a by A12, A10, A26, A7, A8, A1, A33, A34, Def3; ::_thesis: verum
end;
hence  (x1 '=' x2) / (y1,y2) = z1 '=' z2 by A22, A21, A6, FUNCT_1:2; ::_thesis: verum
end;
hence  ( ( ( 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 ) ) implies (x1 '=' x2) / (y1,y2) = z1 '=' z2 ) by A23, A27, A30; ::_thesis: verum
end;

theorem Th153: :: ZF_LANG1:153
for x1, x2, y1, y2 being Variable ex z1, z2 being Variable st (x1 '=' x2) / (y1,y2) = z1 '=' z2
proof
let x1, x2, y1, y2 be Variable; ::_thesis: ex z1, z2 being Variable st (x1 '=' x2) / (y1,y2) = z1 '=' z2
 ( ( x1 <> y1 & x2 <> y1 ) or ( x1 = y1 & x2 <> y1 ) or ( x1 <> y1 & x2 = y1 ) or ( x1 = y1 & x2 = y1 ) ) ;
then consider z1, z2 being Variable such that
A1: ( ( 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 ) ) ;
take  z1 ; ::_thesis: ex z2 being Variable st (x1 '=' x2) / (y1,y2) = z1 '=' z2
take  z2 ; ::_thesis: (x1 '=' x2) / (y1,y2) = z1 '=' z2
thus  (x1 '=' x2) / (y1,y2) = z1 '=' z2 by A1, Th152; ::_thesis: verum
end;

theorem Th154: :: ZF_LANG1:154
for x1, x2, y1, y2, z1, z2 being Variable holds
( (x1 'in' x2) / (y1,y2) = z1 'in' z2 iff ( ( x1 <> y1 & x2 <> y1 & z1 = x1 & z2 = x2 ) or ( x1 = y1 & x2 <> y1 & z1 = y2 & z2 = x2 ) or ( x1 <> y1 & x2 = y1 & z1 = x1 & z2 = y2 ) or ( x1 = y1 & x2 = y1 & z1 = y2 & z2 = y2 ) ) )
proof
let x1, x2, y1, y2, z1, z2 be Variable; ::_thesis: ( (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 ) ) )
set H = x1 'in' x2;
set Hz = z1 'in' z2;
set f = (x1 'in' x2) / (y1,y2);
A1: ( (x1 'in' x2) . 1 = 1 & y1 <> 1 ) by Th135, ZF_LANG:15;
 x1 'in' x2 is being_membership by ZF_LANG:5;
then A2: x1 'in' x2 is atomic by ZF_LANG:def_15;
then A3: len (x1 'in' x2) = 3 by ZF_LANG:11;
then A4: dom (x1 'in' x2) = {1,2,3} by FINSEQ_1:def_3, FINSEQ_3:1;
 z1 'in' z2 is being_membership by ZF_LANG:5;
then A5: z1 'in' z2 is atomic by ZF_LANG:def_15;
then  len (z1 'in' z2) = 3 by ZF_LANG:11;
then A6: dom (z1 'in' z2) = Seg 3 by FINSEQ_1:def_3;
 Var1 (z1 'in' z2) = z1 by Th2;
then A7: (z1 'in' z2) . 2 = z1 by A5, ZF_LANG:35;
 Var2 (z1 'in' z2) = z2 by Th2;
then A8: (z1 'in' z2) . 3 = z2 by A5, ZF_LANG:35;
A9: Var2 (x1 'in' x2) = x2 by Th2;
then A10: (x1 'in' x2) . 3 = x2 by A2, ZF_LANG:35;
A11: Var1 (x1 'in' x2) = x1 by Th2;
then A12: (x1 'in' x2) . 2 = x1 by A2, ZF_LANG:35;
thus  ( not (x1 'in' x2) / (y1,y2) = z1 'in' z2 or ( 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 ) ) ::_thesis: ( ( ( 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 ) ) implies (x1 'in' x2) / (y1,y2) = z1 'in' z2 )
proof
assume A13: (x1 'in' x2) / (y1,y2) = z1 'in' z2 ; ::_thesis: ( ( 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 ) )
percases ( ( x1 <> y1 & x2 <> y1 ) or ( x1 = y1 & x2 <> y1 ) or ( x1 <> y1 & x2 = y1 ) or ( x1 = y1 & x2 = y1 ) ) ;
caseA14: ( x1 <> y1 & x2 <> y1 ) ; ::_thesis: ( z1 = x1 & z2 = x2 )
 ( 2 in dom (x1 'in' x2) & 3 in dom (x1 'in' x2) ) by A4, ENUMSET1:def_1;
hence  ( z1 = x1 & z2 = x2 ) by A12, A10, A7, A8, A13, A14, Def3; ::_thesis: verum
end;
caseA15: ( x1 = y1 & x2 <> y1 ) ; ::_thesis: ( z1 = y2 & z2 = x2 )
A16: ( 2 in dom (x1 'in' x2) & 3 in dom (x1 'in' x2) ) by A4, ENUMSET1:def_1;
 (x1 'in' x2) . 2 = y1 by A2, A11, A15, ZF_LANG:35;
hence  ( z1 = y2 & z2 = x2 ) by A10, A7, A8, A13, A15, A16, Def3; ::_thesis: verum
end;
caseA17: ( x1 <> y1 & x2 = y1 ) ; ::_thesis: ( z1 = x1 & z2 = y2 )
A18: ( 2 in dom (x1 'in' x2) & 3 in dom (x1 'in' x2) ) by A4, ENUMSET1:def_1;
 (x1 'in' x2) . 3 = y1 by A2, A9, A17, ZF_LANG:35;
hence  ( z1 = x1 & z2 = y2 ) by A12, A7, A8, A13, A17, A18, Def3; ::_thesis: verum
end;
caseA19: ( x1 = y1 & x2 = y1 ) ; ::_thesis: ( z1 = y2 & z2 = y2 )
A20: ( 2 in dom (x1 'in' x2) & 3 in dom (x1 'in' x2) ) by A4, ENUMSET1:def_1;
 ( (x1 'in' x2) . 2 = y1 & (x1 'in' x2) . 3 = y1 ) by A2, A11, A9, A19, ZF_LANG:35;
hence  ( z1 = y2 & z2 = y2 ) by A7, A8, A13, A20, Def3; ::_thesis: verum
end;
end;
end;
A21: dom (x1 'in' x2) = Seg 3 by A3, FINSEQ_1:def_3;
A22: dom ((x1 'in' x2) / (y1,y2)) = dom (x1 'in' x2) by Def3;
A23: now__::_thesis:_(_x1_<>_y1_&_x2_<>_y1_&_z1_=_x1_&_z2_=_x2_implies_(x1_'in'_x2)_/_(y1,y2)_=_z1_'in'_z2_)
assume A24: ( x1 <> y1 & x2 <> y1 & z1 = x1 & z2 = x2 ) ; ::_thesis: (x1 'in' x2) / (y1,y2) = z1 'in' z2
now__::_thesis:_for_a_being_set_st_a_in_dom_(x1_'in'_x2)_holds_
(z1_'in'_z2)_._a_=_((x1_'in'_x2)_/_(y1,y2))_._a
let a be set ; ::_thesis: ( a in dom (x1 'in' x2) implies (z1 'in' z2) . a = ((x1 'in' x2) / (y1,y2)) . a )
assume A25: a in dom (x1 'in' x2) ; ::_thesis: (z1 'in' z2) . a = ((x1 'in' x2) / (y1,y2)) . a
then  ( a = 1 or a = 2 or a = 3 ) by A4, ENUMSET1:def_1;
hence  (z1 'in' z2) . a = ((x1 'in' x2) / (y1,y2)) . a by A12, A10, A1, A24, A25, Def3; ::_thesis: verum
end;
hence  (x1 'in' x2) / (y1,y2) = z1 'in' z2 by A22, A21, A6, FUNCT_1:2; ::_thesis: verum
end;
A26: (z1 'in' z2) . 1 = 1 by ZF_LANG:15;
A27: now__::_thesis:_(_x1_<>_y1_&_x2_=_y1_&_z1_=_x1_&_z2_=_y2_implies_(x1_'in'_x2)_/_(y1,y2)_=_z1_'in'_z2_)
assume A28: ( x1 <> y1 & x2 = y1 & z1 = x1 & z2 = y2 ) ; ::_thesis: (x1 'in' x2) / (y1,y2) = z1 'in' z2
now__::_thesis:_for_a_being_set_st_a_in_dom_(x1_'in'_x2)_holds_
(z1_'in'_z2)_._a_=_((x1_'in'_x2)_/_(y1,y2))_._a
let a be set ; ::_thesis: ( a in dom (x1 'in' x2) implies (z1 'in' z2) . a = ((x1 'in' x2) / (y1,y2)) . a )
assume A29: a in dom (x1 'in' x2) ; ::_thesis: (z1 'in' z2) . a = ((x1 'in' x2) / (y1,y2)) . a
then  ( a = 1 or a = 2 or a = 3 ) by A4, ENUMSET1:def_1;
hence  (z1 'in' z2) . a = ((x1 'in' x2) / (y1,y2)) . a by A12, A10, A26, A7, A8, A1, A28, A29, Def3; ::_thesis: verum
end;
hence  (x1 'in' x2) / (y1,y2) = z1 'in' z2 by A22, A21, A6, FUNCT_1:2; ::_thesis: verum
end;
A30: now__::_thesis:_(_x1_=_y1_&_x2_=_y1_&_z1_=_y2_&_z2_=_y2_implies_(x1_'in'_x2)_/_(y1,y2)_=_z1_'in'_z2_)
assume A31: ( x1 = y1 & x2 = y1 & z1 = y2 & z2 = y2 ) ; ::_thesis: (x1 'in' x2) / (y1,y2) = z1 'in' z2
now__::_thesis:_for_a_being_set_st_a_in_dom_(x1_'in'_x2)_holds_
(z1_'in'_z2)_._a_=_((x1_'in'_x2)_/_(y1,y2))_._a
let a be set ; ::_thesis: ( a in dom (x1 'in' x2) implies (z1 'in' z2) . a = ((x1 'in' x2) / (y1,y2)) . a )
assume A32: a in dom (x1 'in' x2) ; ::_thesis: (z1 'in' z2) . a = ((x1 'in' x2) / (y1,y2)) . a
then  ( a = 1 or a = 2 or a = 3 ) by A4, ENUMSET1:def_1;
hence  (z1 'in' z2) . a = ((x1 'in' x2) / (y1,y2)) . a by A12, A10, A26, A7, A8, A1, A31, A32, Def3; ::_thesis: verum
end;
hence  (x1 'in' x2) / (y1,y2) = z1 'in' z2 by A22, A21, A6, FUNCT_1:2; ::_thesis: verum
end;
now__::_thesis:_(_x1_=_y1_&_x2_<>_y1_&_z1_=_y2_&_z2_=_x2_implies_(x1_'in'_x2)_/_(y1,y2)_=_z1_'in'_z2_)
assume A33: ( x1 = y1 & x2 <> y1 & z1 = y2 & z2 = x2 ) ; ::_thesis: (x1 'in' x2) / (y1,y2) = z1 'in' z2
now__::_thesis:_for_a_being_set_st_a_in_dom_(x1_'in'_x2)_holds_
(z1_'in'_z2)_._a_=_((x1_'in'_x2)_/_(y1,y2))_._a
let a be set ; ::_thesis: ( a in dom (x1 'in' x2) implies (z1 'in' z2) . a = ((x1 'in' x2) / (y1,y2)) . a )
assume A34: a in dom (x1 'in' x2) ; ::_thesis: (z1 'in' z2) . a = ((x1 'in' x2) / (y1,y2)) . a
then  ( a = 1 or a = 2 or a = 3 ) by A4, ENUMSET1:def_1;
hence  (z1 'in' z2) . a = ((x1 'in' x2) / (y1,y2)) . a by A12, A10, A26, A7, A8, A1, A33, A34, Def3; ::_thesis: verum
end;
hence  (x1 'in' x2) / (y1,y2) = z1 'in' z2 by A22, A21, A6, FUNCT_1:2; ::_thesis: verum
end;
hence  ( ( ( 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 ) ) implies (x1 'in' x2) / (y1,y2) = z1 'in' z2 ) by A23, A27, A30; ::_thesis: verum
end;

theorem Th155: :: ZF_LANG1:155
for x1, x2, y1, y2 being Variable ex z1, z2 being Variable st (x1 'in' x2) / (y1,y2) = z1 'in' z2
proof
let x1, x2, y1, y2 be Variable; ::_thesis: ex z1, z2 being Variable st (x1 'in' x2) / (y1,y2) = z1 'in' z2
 ( ( x1 <> y1 & x2 <> y1 ) or ( x1 = y1 & x2 <> y1 ) or ( x1 <> y1 & x2 = y1 ) or ( x1 = y1 & x2 = y1 ) ) ;
then consider z1, z2 being Variable such that
A1: ( ( 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 ) ) ;
take  z1 ; ::_thesis: ex z2 being Variable st (x1 'in' x2) / (y1,y2) = z1 'in' z2
take  z2 ; ::_thesis: (x1 'in' x2) / (y1,y2) = z1 'in' z2
thus  (x1 'in' x2) / (y1,y2) = z1 'in' z2 by A1, Th154; ::_thesis: verum
end;

theorem Th156: :: ZF_LANG1:156
for F, H being ZF-formula
for x, y being Variable holds
( 'not' F = ('not' H) / (x,y) iff F = H / (x,y) )
proof
let F, H be ZF-formula; ::_thesis: for x, y being Variable holds
( 'not' F = ('not' H) / (x,y) iff F = H / (x,y) )
let x, y be Variable; ::_thesis: ( 'not' F = ('not' H) / (x,y) iff F = H / (x,y) )
set N = ('not' H) / (x,y);
A1: len <*2*> = 1 by FINSEQ_1:39;
A2: ( dom ('not' F) = Seg (len ('not' F)) & dom ('not' H) = Seg (len ('not' H)) ) by FINSEQ_1:def_3;
A3: ( len ('not' F) = (len <*2*>) + (len F) & len ('not' H) = (len <*2*>) + (len H) ) by FINSEQ_1:22;
A4: ( dom F = Seg (len F) & dom H = Seg (len H) ) by FINSEQ_1:def_3;
thus  ( 'not' F = ('not' H) / (x,y) implies F = H / (x,y) ) ::_thesis: ( F = H / (x,y) implies 'not' F = ('not' H) / (x,y) )
proof
assume A5: 'not' F = ('not' H) / (x,y) ; ::_thesis: F = H / (x,y)
then A6: dom ('not' F) = dom ('not' H) by Def3;
then A7: len ('not' F) = len ('not' H) by FINSEQ_3:29;
A8: now__::_thesis:_for_a_being_set_st_a_in_dom_F_holds_
F_._a_=_(H_/_(x,y))_._a
let a be set ; ::_thesis: ( a in dom F implies F . a = (H / (x,y)) . a )
assume A9: a in dom F ; ::_thesis: F . a = (H / (x,y)) . a
then reconsider i = a as Element of NAT ;
A10: ( F . a = (('not' H) / (x,y)) . (1 + i) & 1 + i in dom (('not' H) / (x,y)) ) by A1, A5, A9, FINSEQ_1:28, FINSEQ_1:def_7;
A11: ('not' H) . (1 + i) = H . a by A1, A4, A3, A7, A9, FINSEQ_1:def_7;
then A12: ( H . a = x implies F . a = y ) by A5, A6, A10, Def3;
A13: ( H . a <> x implies F . a = H . a ) by A5, A6, A10, A11, Def3;
 ( H . a = x implies (H / (x,y)) . a = y ) by A4, A3, A7, A9, Def3;
hence  F . a = (H / (x,y)) . a by A4, A3, A7, A9, A12, A13, Def3; ::_thesis: verum
end;
A14: dom H = dom (H / (x,y)) by Def3;
 dom F = dom H by A3, A7, FINSEQ_3:29;
hence  F = H / (x,y) by A14, A8, FUNCT_1:2; ::_thesis: verum
end;
assume A15: F = H / (x,y) ; ::_thesis: 'not' F = ('not' H) / (x,y)
then A16: dom F = dom H by Def3;
then A17: len F = len H by FINSEQ_3:29;
A18: dom <*2*> = {1} by FINSEQ_1:2, FINSEQ_1:def_8;
A19: now__::_thesis:_for_a_being_set_st_a_in_dom_('not'_F)_holds_
('not'_F)_._a_=_(('not'_H)_/_(x,y))_._a
let a be set ; ::_thesis: ( a in dom ('not' F) implies ('not' F) . a = (('not' H) / (x,y)) . a )
assume A20: a in dom ('not' F) ; ::_thesis: ('not' F) . a = (('not' H) / (x,y)) . a
then reconsider i = a as Element of NAT ;
A21: now__::_thesis:_(_ex_j_being_Nat_st_
(_j_in_dom_F_&_i_=_1_+_j_)_implies_('not'_F)_._a_=_(('not'_H)_/_(x,y))_._a_)
A22: ( ('not' H) . a <> x implies (('not' H) / (x,y)) . a = ('not' H) . a ) by A2, A3, A17, A20, Def3;
given j being Nat such that A23: j in dom F and
A24: i = 1 + j ; ::_thesis: ('not' F) . a = (('not' H) / (x,y)) . a
A25: ( H . j = ('not' H) . i & F . j = ('not' F) . i ) by A1, A16, A23, A24, FINSEQ_1:def_7;
then A26: ( ('not' H) . a = x implies ('not' F) . a = y ) by A15, A16, A23, Def3;
 ( ('not' H) . a <> x implies ('not' F) . a = ('not' H) . a ) by A15, A16, A23, A25, Def3;
hence  ('not' F) . a = (('not' H) / (x,y)) . a by A2, A3, A17, A20, A26, A22, Def3; ::_thesis: verum
end;
now__::_thesis:_(_i_in_{1}_implies_('not'_F)_._a_=_(('not'_H)_/_(x,y))_._a_)
A27: ( ('not' H) . 1 = 2 & 2 <> x ) by Th135, FINSEQ_1:41;
assume  i in {1} ; ::_thesis: ('not' F) . a = (('not' H) / (x,y)) . a
then A28: i = 1 by TARSKI:def_1;
then  ('not' F) . i = 2 by FINSEQ_1:41;
hence  ('not' F) . a = (('not' H) / (x,y)) . a by A2, A3, A17, A20, A28, A27, Def3; ::_thesis: verum
end;
hence  ('not' F) . a = (('not' H) / (x,y)) . a by A1, A18, A20, A21, FINSEQ_1:25; ::_thesis: verum
end;
 dom ('not' F) = dom (('not' H) / (x,y)) by A2, A3, A17, Def3;
hence  'not' F = ('not' H) / (x,y) by A19, FUNCT_1:2; ::_thesis: verum
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
let G1, H1, G2, H2 be ZF-formula; ::_thesis: for x, y being Variable st G1 = H1 / (x,y) & G2 = H2 / (x,y) holds
G1 '&' G2 = (H1 '&' H2) / (x,y)
let x, y be Variable; ::_thesis: ( G1 = H1 / (x,y) & G2 = H2 / (x,y) implies G1 '&' G2 = (H1 '&' H2) / (x,y) )
set N = (H1 '&' H2) / (x,y);
A1: dom <*3*> = {1} by FINSEQ_1:2, FINSEQ_1:def_8;
A2: ( dom (G1 '&' G2) = Seg (len (G1 '&' G2)) & dom (H1 '&' H2) = Seg (len (H1 '&' H2)) ) by FINSEQ_1:def_3;
A3: len <*3*> = 1 by FINSEQ_1:39;
then A4: len (<*3*> ^ G1) = 1 + (len G1) by FINSEQ_1:22;
then A5: len (G1 '&' G2) = (1 + (len G1)) + (len G2) by FINSEQ_1:22;
A6: len (<*3*> ^ H1) = 1 + (len H1) by A3, FINSEQ_1:22;
then A7: len (H1 '&' H2) = (1 + (len H1)) + (len H2) by FINSEQ_1:22;
A8: dom (<*3*> ^ H1) = Seg (1 + (len H1)) by A6, FINSEQ_1:def_3;
A9: dom ((H1 '&' H2) / (x,y)) = dom (H1 '&' H2) by Def3;
assume that
A10: G1 = H1 / (x,y) and
A11: G2 = H2 / (x,y) ; ::_thesis: G1 '&' G2 = (H1 '&' H2) / (x,y)
A12: dom G1 = dom H1 by A10, Def3;
then A13: len G1 = len H1 by FINSEQ_3:29;
A14: dom G2 = dom H2 by A11, Def3;
then  len G2 = len H2 by FINSEQ_3:29;
then A15: dom ((H1 '&' H2) / (x,y)) = dom (G1 '&' G2) by A2, A5, A7, A13, Def3;
A16: dom (<*3*> ^ G1) = Seg (1 + (len G1)) by A4, FINSEQ_1:def_3;
now__::_thesis:_for_a_being_set_st_a_in_dom_((H1_'&'_H2)_/_(x,y))_holds_
(G1_'&'_G2)_._a_=_((H1_'&'_H2)_/_(x,y))_._a
let a be set ; ::_thesis: ( a in dom ((H1 '&' H2) / (x,y)) implies (G1 '&' G2) . a = ((H1 '&' H2) / (x,y)) . a )
assume A17: a in dom ((H1 '&' H2) / (x,y)) ; ::_thesis: (G1 '&' G2) . a = ((H1 '&' H2) / (x,y)) . a
then reconsider i = a as Element of NAT by A15;
A18: now__::_thesis:_(_i_in_dom_(<*3*>_^_G1)_implies_(G1_'&'_G2)_._a_=_((H1_'&'_H2)_/_(x,y))_._a_)
A19: now__::_thesis:_(_i_in_{1}_implies_((H1_'&'_H2)_/_(x,y))_._a_=_(G1_'&'_G2)_._a_)
assume  i in {1} ; ::_thesis: ((H1 '&' H2) / (x,y)) . a = (G1 '&' G2) . a
then A20: i = 1 by TARSKI:def_1;
 ( (H1 '&' H2) . 1 = 3 & x <> 3 ) by Th135, ZF_LANG:16;
then  ((H1 '&' H2) / (x,y)) . i = 3 by A9, A17, A20, Def3;
hence  ((H1 '&' H2) / (x,y)) . a = (G1 '&' G2) . a by A20, ZF_LANG:16; ::_thesis: verum
end;
assume A21: i in dom (<*3*> ^ G1) ; ::_thesis: (G1 '&' G2) . a = ((H1 '&' H2) / (x,y)) . a
then A22: ( (G1 '&' G2) . i = (<*3*> ^ G1) . i & (H1 '&' H2) . i = (<*3*> ^ H1) . i ) by A16, A8, A13, FINSEQ_1:def_7;
now__::_thesis:_(_ex_j_being_Nat_st_
(_j_in_dom_G1_&_i_=_1_+_j_)_implies_(G1_'&'_G2)_._a_=_((H1_'&'_H2)_/_(x,y))_._a_)
A23: ( (H1 '&' H2) . a <> x implies ((H1 '&' H2) / (x,y)) . a = (H1 '&' H2) . a ) by A9, A17, Def3;
given j being Nat such that A24: j in dom G1 and
A25: i = 1 + j ; ::_thesis: (G1 '&' G2) . a = ((H1 '&' H2) / (x,y)) . a
A26: ( G1 . j = (G1 '&' G2) . i & H1 . j = (H1 '&' H2) . i ) by A3, A12, A22, A24, A25, FINSEQ_1:def_7;
then A27: ( (H1 '&' H2) . a = x implies (G1 '&' G2) . a = y ) by A10, A12, A24, Def3;
 ( (H1 '&' H2) . a <> x implies (G1 '&' G2) . a = (H1 '&' H2) . a ) by A10, A12, A24, A26, Def3;
hence  (G1 '&' G2) . a = ((H1 '&' H2) / (x,y)) . a by A9, A17, A27, A23, Def3; ::_thesis: verum
end;
hence  (G1 '&' G2) . a = ((H1 '&' H2) / (x,y)) . a by A3, A1, A21, A19, FINSEQ_1:25; ::_thesis: verum
end;
now__::_thesis:_(_ex_j_being_Nat_st_
(_j_in_dom_G2_&_i_=_(1_+_(len_G1))_+_j_)_implies_(G1_'&'_G2)_._a_=_((H1_'&'_H2)_/_(x,y))_._a_)
A28: ( (H1 '&' H2) . a <> x implies ((H1 '&' H2) / (x,y)) . a = (H1 '&' H2) . a ) by A9, A17, Def3;
given j being Nat such that A29: j in dom G2 and
A30: i = (1 + (len G1)) + j ; ::_thesis: (G1 '&' G2) . a = ((H1 '&' H2) / (x,y)) . a
A31: ( G2 . j = (G1 '&' G2) . i & H2 . j = (H1 '&' H2) . i ) by A4, A6, A14, A13, A29, A30, FINSEQ_1:def_7;
then A32: ( (H1 '&' H2) . a = x implies (G1 '&' G2) . a = y ) by A11, A14, A29, Def3;
 ( (H1 '&' H2) . a <> x implies (G1 '&' G2) . a = (H1 '&' H2) . a ) by A11, A14, A29, A31, Def3;
hence  (G1 '&' G2) . a = ((H1 '&' H2) / (x,y)) . a by A9, A17, A28, A32, Def3; ::_thesis: verum
end;
hence  (G1 '&' G2) . a = ((H1 '&' H2) / (x,y)) . a by A4, A15, A17, A18, FINSEQ_1:25; ::_thesis: verum
end;
hence  G1 '&' G2 = (H1 '&' H2) / (x,y) by A15, FUNCT_1:2; ::_thesis: verum
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
let F, H be ZF-formula; ::_thesis: 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)
let x, y, z, s be Variable; ::_thesis: ( F = H / (x,y) & ( ( z = s & s <> x ) or ( z = y & s = x ) ) implies All (z,F) = (All (s,H)) / (x,y) )
set N = (All (s,H)) / (x,y);
A1: ( len <*4*> = 1 & 1 + 1 = 2 ) by FINSEQ_1:39;
 len <*s*> = 1 by FINSEQ_1:39;
then A2: len (<*4*> ^ <*s*>) = 2 by A1, FINSEQ_1:22;
then A3: dom (<*4*> ^ <*s*>) = {1,2} by FINSEQ_1:2, FINSEQ_1:def_3;
 len (All (s,H)) = 2 + (len H) by A2, FINSEQ_1:22;
then A4: dom (All (s,H)) = Seg (2 + (len H)) by FINSEQ_1:def_3;
A5: ( <*4*> ^ <*z*> = <*4,z*> & <*4*> ^ <*s*> = <*4,s*> ) by FINSEQ_1:def_9;
A6: dom ((All (s,H)) / (x,y)) = dom (All (s,H)) by Def3;
assume that
A7: F = H / (x,y) and
A8: ( ( z = s & s <> x ) or ( z = y & s = x ) ) ; ::_thesis: All (z,F) = (All (s,H)) / (x,y)
A9: dom F = dom H by A7, Def3;
 len <*z*> = 1 by FINSEQ_1:39;
then A10: len (<*4*> ^ <*z*>) = 2 by A1, FINSEQ_1:22;
then A11: dom (<*4*> ^ <*z*>) = {1,2} by FINSEQ_1:2, FINSEQ_1:def_3;
A12: now__::_thesis:_for_a_being_set_st_a_in_dom_((All_(s,H))_/_(x,y))_holds_
(All_(z,F))_._a_=_((All_(s,H))_/_(x,y))_._a
let a be set ; ::_thesis: ( a in dom ((All (s,H)) / (x,y)) implies (All (z,F)) . a = ((All (s,H)) / (x,y)) . a )
assume A13: a in dom ((All (s,H)) / (x,y)) ; ::_thesis: (All (z,F)) . a = ((All (s,H)) / (x,y)) . a
then reconsider a1 = a as Element of NAT by A6;
A14: now__::_thesis:_(_a_in_{1,2}_implies_(All_(z,F))_._a_=_((All_(s,H))_/_(x,y))_._a_)
A15: ( x <> 4 & <*4,z*> . 1 = 4 ) by Th135, FINSEQ_1:44;
A16: ( <*4,s*> . 1 = 4 & <*4,z*> . 2 = z ) by FINSEQ_1:44;
A17: <*4,s*> . 2 = s by FINSEQ_1:44;
assume A18: a in {1,2} ; ::_thesis: (All (z,F)) . a = ((All (s,H)) / (x,y)) . a
then A19: ( a = 1 or a = 2 ) by TARSKI:def_2;
 ( (All (z,F)) . a1 = <*4,z*> . a1 & (All (s,H)) . a1 = <*4,s*> . a1 ) by A11, A3, A5, A18, FINSEQ_1:def_7;
hence  (All (z,F)) . a = ((All (s,H)) / (x,y)) . a by A8, A6, A13, A19, A15, A16, A17, Def3; ::_thesis: verum
end;
now__::_thesis:_(_ex_i_being_Nat_st_
(_i_in_dom_H_&_a1_=_2_+_i_)_implies_(All_(z,F))_._a_=_((All_(s,H))_/_(x,y))_._a_)
A20: ( (All (s,H)) . a <> x implies ((All (s,H)) / (x,y)) . a = (All (s,H)) . a ) by A6, A13, Def3;
given i being Nat such that A21: i in dom H and
A22: a1 = 2 + i ; ::_thesis: (All (z,F)) . a = ((All (s,H)) / (x,y)) . a
A23: ( (All (z,F)) . a = F . i & (All (s,H)) . a = H . i ) by A10, A2, A9, A21, A22, FINSEQ_1:def_7;
then A24: ( (All (s,H)) . a = x implies (All (z,F)) . a = y ) by A7, A21, Def3;
 ( (All (s,H)) . a <> x implies (All (z,F)) . a = (All (s,H)) . a ) by A7, A21, A23, Def3;
hence  (All (z,F)) . a = ((All (s,H)) / (x,y)) . a by A6, A13, A24, A20, Def3; ::_thesis: verum
end;
hence  (All (z,F)) . a = ((All (s,H)) / (x,y)) . a by A2, A3, A6, A13, A14, FINSEQ_1:25; ::_thesis: verum
end;
 len (All (z,F)) = 2 + (len F) by A10, FINSEQ_1:22;
then  dom (All (z,F)) = Seg (2 + (len F)) by FINSEQ_1:def_3;
then  dom (All (s,H)) = dom (All (z,F)) by A4, A9, FINSEQ_3:29;
hence  All (z,F) = (All (s,H)) / (x,y) by A6, A12, FUNCT_1:2; ::_thesis: verum
end;

theorem Th157: :: ZF_LANG1:157
for H being ZF-formula
for x, y being Variable holds H / (x,y) in WFF
proof
let H be ZF-formula; ::_thesis: for x, y being Variable holds H / (x,y) in WFF
let x, y be Variable; ::_thesis: H / (x,y) in WFF
defpred S1[ ZF-formula] means $1 / (x,y) in WFF ;
A1: for H being ZF-formula st S1[H] holds
S1[ 'not' H]
proof
let H be ZF-formula; ::_thesis: ( S1[H] implies S1[ 'not' H] )
assume  H / (x,y) in WFF ; ::_thesis: S1[ 'not' H]
then reconsider F = H / (x,y) as ZF-formula by ZF_LANG:4;
 'not' F = ('not' H) / (x,y) by Th156;
hence  S1[ 'not' H] by ZF_LANG:4; ::_thesis: verum
end;
A2: for H1, H2 being ZF-formula st S1[H1] & S1[H2] holds
S1[H1 '&' H2]
proof
let H1, H2 be ZF-formula; ::_thesis: ( S1[H1] & S1[H2] implies S1[H1 '&' H2] )
assume  ( H1 / (x,y) in WFF & H2 / (x,y) in WFF ) ; ::_thesis: S1[H1 '&' H2]
then reconsider F1 = H1 / (x,y), F2 = H2 / (x,y) as ZF-formula by ZF_LANG:4;
 F1 '&' F2 = (H1 '&' H2) / (x,y) by Lm1;
hence  S1[H1 '&' H2] by ZF_LANG:4; ::_thesis: verum
end;
A3: for H being ZF-formula
for z being Variable st S1[H] holds
S1[ All (z,H)]
proof
let H be ZF-formula; ::_thesis: for z being Variable st S1[H] holds
S1[ All (z,H)]
let z be Variable; ::_thesis: ( S1[H] implies S1[ All (z,H)] )
assume  H / (x,y) in WFF ; ::_thesis: S1[ All (z,H)]
then reconsider F = H / (x,y) as ZF-formula by ZF_LANG:4;
 ( z <> x or z = x ) ;
then consider s being Variable such that
A4: ( ( s = z & z <> x ) or ( s = y & z = x ) ) ;
 All (s,F) = (All (z,H)) / (x,y) by A4, Lm2;
hence  S1[ All (z,H)] by ZF_LANG:4; ::_thesis: verum
end;
A5: for x1, x2 being Variable holds
( S1[x1 '=' x2] & S1[x1 'in' x2] )
proof
let x1, x2 be Variable; ::_thesis: ( S1[x1 '=' x2] & S1[x1 'in' x2] )
 ( ex y1, y2 being Variable st (x1 '=' x2) / (x,y) = y1 '=' y2 & ex z1, z2 being Variable st (x1 'in' x2) / (x,y) = z1 'in' z2 ) by Th153, Th155;
hence  ( S1[x1 '=' x2] & S1[x1 'in' x2] ) by ZF_LANG:4; ::_thesis: verum
end;
 for H being ZF-formula holds S1[H] from ZF_LANG1:sch_1(A5, A1, A2, A3);
hence  H / (x,y) in WFF ; ::_thesis: verum
end;

definition
let H be ZF-formula;
let x, y be Variable;
:: original: /
redefine funcH / (x,y) ->  ZF-formula;
coherence
 H / (x,y) is ZF-formula
proof
A1: dom (H / (x,y)) = dom H by Def3;
 dom H = Seg (len H) by FINSEQ_1:def_3;
then reconsider f = H / (x,y) as FinSequence by A1, FINSEQ_1:def_2;
A2: for a being set st a in dom H holds
( ( H . a = x implies (H / (x,y)) . a = y ) & ( H . a <> x implies (H / (x,y)) . a = H . a ) ) by Def3;
 rng f c= NAT
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in rng f or a in NAT )
assume  a in rng f ; ::_thesis: a in NAT
then consider b being set  such that
A3: b in dom f and
A4: a = f . b by FUNCT_1:def_3;
 ( rng H c= NAT & H . b in rng H ) by A1, A3, FINSEQ_1:def_4, FUNCT_1:def_3;
then  ( a = y or ( a = H . b & H . b in NAT ) ) by A1, A2, A3, A4;
hence  a in NAT ; ::_thesis: verum
end;
then reconsider f = f as FinSequence of NAT by FINSEQ_1:def_4;
 f in WFF by Th157;
hence  H / (x,y) is ZF-formula by ZF_LANG:4; ::_thesis: verum
end;
end;

theorem Th158: :: ZF_LANG1:158
for G1, G2, H1, H2 being ZF-formula
for x, y being Variable holds
( G1 '&' G2 = (H1 '&' H2) / (x,y) iff ( G1 = H1 / (x,y) & G2 = H2 / (x,y) ) )
proof
let G1, G2, H1, H2 be ZF-formula; ::_thesis: for x, y being Variable holds
( G1 '&' G2 = (H1 '&' H2) / (x,y) iff ( G1 = H1 / (x,y) & G2 = H2 / (x,y) ) )
let x, y be Variable; ::_thesis: ( G1 '&' G2 = (H1 '&' H2) / (x,y) iff ( G1 = H1 / (x,y) & G2 = H2 / (x,y) ) )
thus  ( G1 '&' G2 = (H1 '&' H2) / (x,y) implies ( G1 = H1 / (x,y) & G2 = H2 / (x,y) ) ) ::_thesis: ( G1 = H1 / (x,y) & G2 = H2 / (x,y) implies G1 '&' G2 = (H1 '&' H2) / (x,y) )
proof
assume  G1 '&' G2 = (H1 '&' H2) / (x,y) ; ::_thesis: ( G1 = H1 / (x,y) & G2 = H2 / (x,y) )
then  G1 '&' G2 = (H1 / (x,y)) '&' (H2 / (x,y)) by Lm1;
hence  ( G1 = H1 / (x,y) & G2 = H2 / (x,y) ) by ZF_LANG:30; ::_thesis: verum
end;
thus  ( G1 = H1 / (x,y) & G2 = H2 / (x,y) implies G1 '&' G2 = (H1 '&' H2) / (x,y) ) by Lm1; ::_thesis: verum
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) )
proof
let G, H be ZF-formula; ::_thesis: for z, x, y being Variable st z <> x holds
( All (z,G) = (All (z,H)) / (x,y) iff G = H / (x,y) )
let z, x, y be Variable; ::_thesis: ( z <> x implies ( All (z,G) = (All (z,H)) / (x,y) iff G = H / (x,y) ) )
assume A1: z <> x ; ::_thesis: ( All (z,G) = (All (z,H)) / (x,y) iff G = H / (x,y) )
thus  ( All (z,G) = (All (z,H)) / (x,y) implies G = H / (x,y) ) ::_thesis: ( G = H / (x,y) implies All (z,G) = (All (z,H)) / (x,y) )
proof
assume  All (z,G) = (All (z,H)) / (x,y) ; ::_thesis: G = H / (x,y)
then  All (z,G) = All (z,(H / (x,y))) by A1, Lm2;
hence  G = H / (x,y) by ZF_LANG:3; ::_thesis: verum
end;
thus  ( G = H / (x,y) implies All (z,G) = (All (z,H)) / (x,y) ) by A1, Lm2; ::_thesis: verum
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) )
proof
let G, H be ZF-formula; ::_thesis: for y, x being Variable holds
( All (y,G) = (All (x,H)) / (x,y) iff G = H / (x,y) )
let y, x be Variable; ::_thesis: ( All (y,G) = (All (x,H)) / (x,y) iff G = H / (x,y) )
thus  ( All (y,G) = (All (x,H)) / (x,y) implies G = H / (x,y) ) ::_thesis: ( G = H / (x,y) implies All (y,G) = (All (x,H)) / (x,y) )
proof
assume  All (y,G) = (All (x,H)) / (x,y) ; ::_thesis: G = H / (x,y)
then  All (y,G) = All (y,(H / (x,y))) by Lm2;
hence  G = H / (x,y) by ZF_LANG:3; ::_thesis: verum
end;
thus  ( G = H / (x,y) implies All (y,G) = (All (x,H)) / (x,y) ) by Lm2; ::_thesis: verum
end;

theorem Th161: :: ZF_LANG1:161
for G1, G2, H1, H2 being ZF-formula
for x, y being Variable holds
( G1 'or' G2 = (H1 'or' H2) / (x,y) iff ( G1 = H1 / (x,y) & G2 = H2 / (x,y) ) )
proof
let G1, G2, H1, H2 be ZF-formula; ::_thesis: for x, y being Variable holds
( G1 'or' G2 = (H1 'or' H2) / (x,y) iff ( G1 = H1 / (x,y) & G2 = H2 / (x,y) ) )
let x, y be Variable; ::_thesis: ( G1 'or' G2 = (H1 'or' H2) / (x,y) iff ( G1 = H1 / (x,y) & G2 = H2 / (x,y) ) )
 ( ( 'not' G1 = ('not' H1) / (x,y) & 'not' G2 = ('not' H2) / (x,y) ) iff ('not' G1) '&' ('not' G2) = (('not' H1) '&' ('not' H2)) / (x,y) ) by Th158;
hence  ( G1 'or' G2 = (H1 'or' H2) / (x,y) iff ( G1 = H1 / (x,y) & G2 = H2 / (x,y) ) ) by Th156; ::_thesis: verum
end;

theorem Th162: :: ZF_LANG1:162
for G1, G2, H1, H2 being ZF-formula
for x, y being Variable holds
( G1 => G2 = (H1 => H2) / (x,y) iff ( G1 = H1 / (x,y) & G2 = H2 / (x,y) ) )
proof
let G1, G2, H1, H2 be ZF-formula; ::_thesis: for x, y being Variable holds
( G1 => G2 = (H1 => H2) / (x,y) iff ( G1 = H1 / (x,y) & G2 = H2 / (x,y) ) )
let x, y be Variable; ::_thesis: ( G1 => G2 = (H1 => H2) / (x,y) iff ( G1 = H1 / (x,y) & G2 = H2 / (x,y) ) )
 ( ( G1 = H1 / (x,y) & 'not' G2 = ('not' H2) / (x,y) ) iff G1 '&' ('not' G2) = (H1 '&' ('not' H2)) / (x,y) ) by Th158;
hence  ( G1 => G2 = (H1 => H2) / (x,y) iff ( G1 = H1 / (x,y) & G2 = H2 / (x,y) ) ) by Th156; ::_thesis: verum
end;

theorem Th163: :: ZF_LANG1:163
for G1, G2, H1, H2 being ZF-formula
for x, y being Variable holds
( G1 <=> G2 = (H1 <=> H2) / (x,y) iff ( G1 = H1 / (x,y) & G2 = H2 / (x,y) ) )
proof
let G1, G2, H1, H2 be ZF-formula; ::_thesis: for x, y being Variable holds
( G1 <=> G2 = (H1 <=> H2) / (x,y) iff ( G1 = H1 / (x,y) & G2 = H2 / (x,y) ) )
let x, y be Variable; ::_thesis: ( G1 <=> G2 = (H1 <=> H2) / (x,y) iff ( G1 = H1 / (x,y) & G2 = H2 / (x,y) ) )
 ( G1 <=> G2 = (H1 <=> H2) / (x,y) iff ( G1 => G2 = (H1 => H2) / (x,y) & G2 => G1 = (H2 => H1) / (x,y) ) ) by Th158;
hence  ( G1 <=> G2 = (H1 <=> H2) / (x,y) iff ( G1 = H1 / (x,y) & G2 = H2 / (x,y) ) ) by Th162; ::_thesis: verum
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) )
proof
let G, H be ZF-formula; ::_thesis: for z, x, y being Variable st z <> x holds
( Ex (z,G) = (Ex (z,H)) / (x,y) iff G = H / (x,y) )
let z, x, y be Variable; ::_thesis: ( z <> x implies ( Ex (z,G) = (Ex (z,H)) / (x,y) iff G = H / (x,y) ) )
assume  z <> x ; ::_thesis: ( Ex (z,G) = (Ex (z,H)) / (x,y) iff G = H / (x,y) )
then  ( 'not' G = ('not' H) / (x,y) iff All (z,('not' G)) = (All (z,('not' H))) / (x,y) ) by Th159;
hence  ( Ex (z,G) = (Ex (z,H)) / (x,y) iff G = H / (x,y) ) by Th156; ::_thesis: verum
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) )
proof
let G, H be ZF-formula; ::_thesis: for y, x being Variable holds
( Ex (y,G) = (Ex (x,H)) / (x,y) iff G = H / (x,y) )
let y, x be Variable; ::_thesis: ( Ex (y,G) = (Ex (x,H)) / (x,y) iff G = H / (x,y) )
 ( 'not' G = ('not' H) / (x,y) iff All (y,('not' G)) = (All (x,('not' H))) / (x,y) ) by Th160;
hence  ( Ex (y,G) = (Ex (x,H)) / (x,y) iff G = H / (x,y) ) by Th156; ::_thesis: verum
end;

theorem :: ZF_LANG1:166
for H being ZF-formula
for x, y being Variable holds
( H is being_equality iff H / (x,y) is being_equality )
proof
let H be ZF-formula; ::_thesis: for x, y being Variable holds
( H is being_equality iff H / (x,y) is being_equality )
let x, y be Variable; ::_thesis: ( H is being_equality iff H / (x,y) is being_equality )
thus  ( H is being_equality implies H / (x,y) is being_equality ) ::_thesis: ( H / (x,y) is being_equality implies H is being_equality )
proof
given x1, x2 being Variable such that A1: H = x1 '=' x2 ; :: according to ZF_LANG:def_10 ::_thesis: H / (x,y) is being_equality
 ex z1, z2 being Variable st H / (x,y) = z1 '=' z2 by A1, Th153;
hence  H / (x,y) is being_equality by ZF_LANG:5; ::_thesis: verum
end;
assume  H / (x,y) is being_equality ; ::_thesis: H is being_equality
then A2: (H / (x,y)) . 1 = 0 by ZF_LANG:18;
 3 <= len H by ZF_LANG:13;
then  1 <= len H by XXREAL_0:2;
then A3: 1 in dom H by FINSEQ_3:25;
 y <> 0 by Th135;
then  H . 1 <> x by A2, A3, Def3;
then  0 = H . 1 by A2, A3, Def3;
hence  H is being_equality by ZF_LANG:24; ::_thesis: verum
end;

theorem :: ZF_LANG1:167
for H being ZF-formula
for x, y being Variable holds
( H is being_membership iff H / (x,y) is being_membership )
proof
let H be ZF-formula; ::_thesis: for x, y being Variable holds
( H is being_membership iff H / (x,y) is being_membership )
let x, y be Variable; ::_thesis: ( H is being_membership iff H / (x,y) is being_membership )
thus  ( H is being_membership implies H / (x,y) is being_membership ) ::_thesis: ( H / (x,y) is being_membership implies H is being_membership )
proof
given x1, x2 being Variable such that A1: H = x1 'in' x2 ; :: according to ZF_LANG:def_11 ::_thesis: H / (x,y) is being_membership
 ex z1, z2 being Variable st H / (x,y) = z1 'in' z2 by A1, Th155;
hence  H / (x,y) is being_membership by ZF_LANG:5; ::_thesis: verum
end;
assume  H / (x,y) is being_membership ; ::_thesis: H is being_membership
then A2: (H / (x,y)) . 1 = 1 by ZF_LANG:19;
 3 <= len H by ZF_LANG:13;
then  1 <= len H by XXREAL_0:2;
then A3: 1 in dom H by FINSEQ_3:25;
 y <> 1 by Th135;
then  H . 1 <> x by A2, A3, Def3;
then  1 = H . 1 by A2, A3, Def3;
hence  H is being_membership by ZF_LANG:25; ::_thesis: verum
end;

theorem Th168: :: ZF_LANG1:168
for H being ZF-formula
for x, y being Variable holds
( H is negative iff H / (x,y) is negative )
proof
let H be ZF-formula; ::_thesis: for x, y being Variable holds
( H is negative iff H / (x,y) is negative )
let x, y be Variable; ::_thesis: ( H is negative iff H / (x,y) is negative )
thus  ( H is negative implies H / (x,y) is negative ) ::_thesis: ( H / (x,y) is negative implies H is negative )
proof
given H1 being ZF-formula such that A1: H = 'not' H1 ; :: according to ZF_LANG:def_12 ::_thesis: H / (x,y) is negative
 H / (x,y) = 'not' (H1 / (x,y)) by A1, Th156;
hence  H / (x,y) is negative by ZF_LANG:5; ::_thesis: verum
end;
assume  H / (x,y) is negative ; ::_thesis: H is negative
then A2: (H / (x,y)) . 1 = 2 by ZF_LANG:20;
 3 <= len H by ZF_LANG:13;
then  1 <= len H by XXREAL_0:2;
then A3: 1 in dom H by FINSEQ_3:25;
 y <> 2 by Th135;
then  H . 1 <> x by A2, A3, Def3;
then  2 = H . 1 by A2, A3, Def3;
hence  H is negative by ZF_LANG:26; ::_thesis: verum
end;

theorem Th169: :: ZF_LANG1:169
for H being ZF-formula
for x, y being Variable holds
( H is conjunctive iff H / (x,y) is conjunctive )
proof
let H be ZF-formula; ::_thesis: for x, y being Variable holds
( H is conjunctive iff H / (x,y) is conjunctive )
let x, y be Variable; ::_thesis: ( H is conjunctive iff H / (x,y) is conjunctive )
thus  ( H is conjunctive implies H / (x,y) is conjunctive ) ::_thesis: ( H / (x,y) is conjunctive implies H is conjunctive )
proof
given H1, H2 being ZF-formula such that A1: H = H1 '&' H2 ; :: according to ZF_LANG:def_13 ::_thesis: H / (x,y) is conjunctive
 H / (x,y) = (H1 / (x,y)) '&' (H2 / (x,y)) by A1, Th158;
hence  H / (x,y) is conjunctive by ZF_LANG:5; ::_thesis: verum
end;
assume  H / (x,y) is conjunctive ; ::_thesis: H is conjunctive
then A2: (H / (x,y)) . 1 = 3 by ZF_LANG:21;
 3 <= len H by ZF_LANG:13;
then  1 <= len H by XXREAL_0:2;
then A3: 1 in dom H by FINSEQ_3:25;
 y <> 3 by Th135;
then  H . 1 <> x by A2, A3, Def3;
then  3 = H . 1 by A2, A3, Def3;
hence  H is conjunctive by ZF_LANG:27; ::_thesis: verum
end;

theorem Th170: :: ZF_LANG1:170
for H being ZF-formula
for x, y being Variable holds
( H is universal iff H / (x,y) is universal )
proof
let H be ZF-formula; ::_thesis: for x, y being Variable holds
( H is universal iff H / (x,y) is universal )
let x, y be Variable; ::_thesis: ( H is universal iff H / (x,y) is universal )
thus  ( H is universal implies H / (x,y) is universal ) ::_thesis: ( H / (x,y) is universal implies H is universal )
proof
given z being Variable, H1 being ZF-formula such that A1: H = All (z,H1) ; :: according to ZF_LANG:def_14 ::_thesis: H / (x,y) is universal
 ( z = x or z <> x ) ;
then consider s being Variable such that
A2: ( ( z = x & s = y ) or ( z <> x & s = z ) ) ;
 H / (x,y) = All (s,(H1 / (x,y))) by A1, A2, Th159, Th160;
hence  H / (x,y) is universal by ZF_LANG:5; ::_thesis: verum
end;
assume  H / (x,y) is universal ; ::_thesis: H is universal
then A3: (H / (x,y)) . 1 = 4 by ZF_LANG:22;
 3 <= len H by ZF_LANG:13;
then  1 <= len H by XXREAL_0:2;
then A4: 1 in dom H by FINSEQ_3:25;
 y <> 4 by Th135;
then  H . 1 <> x by A3, A4, Def3;
then  4 = H . 1 by A3, A4, Def3;
hence  H is universal by ZF_LANG:28; ::_thesis: verum
end;

theorem :: ZF_LANG1:171
for H being ZF-formula
for x, y being Variable st H is negative holds
the_argument_of (H / (x,y)) = (the_argument_of H) / (x,y)
proof
let H be ZF-formula; ::_thesis: for x, y being Variable st H is negative holds
the_argument_of (H / (x,y)) = (the_argument_of H) / (x,y)
let x, y be Variable; ::_thesis: ( H is negative implies the_argument_of (H / (x,y)) = (the_argument_of H) / (x,y) )
assume A1: H is negative ; ::_thesis: the_argument_of (H / (x,y)) = (the_argument_of H) / (x,y)
then  H / (x,y) is negative by Th168;
then A2: H / (x,y) = 'not' (the_argument_of (H / (x,y))) by ZF_LANG:def_30;
 H = 'not' (the_argument_of H) by A1, ZF_LANG:def_30;
hence  the_argument_of (H / (x,y)) = (the_argument_of H) / (x,y) by A2, Th156; ::_thesis: verum
end;

theorem :: ZF_LANG1:172
for H being ZF-formula
for x, y being Variable st H is conjunctive holds
( the_left_argument_of (H / (x,y)) = (the_left_argument_of H) / (x,y) & the_right_argument_of (H / (x,y)) = (the_right_argument_of H) / (x,y) )
proof
let H be ZF-formula; ::_thesis: 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) )
let x, y be Variable; ::_thesis: ( H is conjunctive implies ( 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) ) )
assume A1: H is conjunctive ; ::_thesis: ( 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) )
then  H / (x,y) is conjunctive by Th169;
then A2: H / (x,y) = (the_left_argument_of (H / (x,y))) '&' (the_right_argument_of (H / (x,y))) by ZF_LANG:40;
 H = (the_left_argument_of H) '&' (the_right_argument_of H) by A1, ZF_LANG:40;
hence  ( 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) ) by A2, Th158; ::_thesis: verum
end;

theorem :: ZF_LANG1:173
for H being ZF-formula
for x, y being Variable st H is universal holds
( the_scope_of (H / (x,y)) = (the_scope_of H) / (x,y) & ( bound_in H = x implies bound_in (H / (x,y)) = y ) & ( bound_in H <> x implies bound_in (H / (x,y)) = bound_in H ) )
proof
let H be ZF-formula; ::_thesis: 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 ) )
let x, y be Variable; ::_thesis: ( H is universal implies ( 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 ) ) )
assume A1: H is universal ; ::_thesis: ( 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 ) )
then  H / (x,y) is universal by Th170;
then A2: H / (x,y) = All ((bound_in (H / (x,y))),(the_scope_of (H / (x,y)))) by ZF_LANG:44;
A3: H = All ((bound_in H),(the_scope_of H)) by A1, ZF_LANG:44;
then A4: ( bound_in H <> x implies H / (x,y) = All ((bound_in H),((the_scope_of H) / (x,y))) ) by Th159;
 ( bound_in H = x implies H / (x,y) = All (y,((the_scope_of H) / (x,y))) ) by A3, Th160;
hence  ( 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 ) ) by A2, A4, ZF_LANG:3; ::_thesis: verum
end;

theorem Th174: :: ZF_LANG1:174
for H being ZF-formula
for x, y being Variable holds
( H is disjunctive iff H / (x,y) is disjunctive )
proof
let H be ZF-formula; ::_thesis: for x, y being Variable holds
( H is disjunctive iff H / (x,y) is disjunctive )
let x, y be Variable; ::_thesis: ( H is disjunctive iff H / (x,y) is disjunctive )
set G = H / (x,y);
thus  ( H is disjunctive implies H / (x,y) is disjunctive ) ::_thesis: ( H / (x,y) is disjunctive implies H is disjunctive )
proof
given H1, H2 being ZF-formula such that A1: H = H1 'or' H2 ; :: according to ZF_LANG:def_20 ::_thesis: H / (x,y) is disjunctive
 H / (x,y) = (H1 / (x,y)) 'or' (H2 / (x,y)) by A1, Th161;
hence  H / (x,y) is disjunctive by ZF_LANG:6; ::_thesis: verum
end;
given G1, G2 being ZF-formula such that A2: H / (x,y) = G1 'or' G2 ; :: according to ZF_LANG:def_20 ::_thesis: H is disjunctive
 H / (x,y) is negative by A2, ZF_LANG:5;
then  H is negative by Th168;
then consider H9 being ZF-formula such that
A3: H = 'not' H9 by ZF_LANG:5;
A4: ('not' G1) '&' ('not' G2) = H9 / (x,y) by A2, A3, Th156;
then  H9 / (x,y) is conjunctive by ZF_LANG:5;
then  H9 is conjunctive by Th169;
then consider H1, H2 being ZF-formula such that
A5: H9 = H1 '&' H2 by ZF_LANG:5;
 'not' G2 = H2 / (x,y) by A4, A5, Th158;
then  H2 / (x,y) is negative by ZF_LANG:5;
then  H2 is negative by Th168;
then consider p2 being ZF-formula such that
A6: H2 = 'not' p2 by ZF_LANG:5;
 'not' G1 = H1 / (x,y) by A4, A5, Th158;
then  H1 / (x,y) is negative by ZF_LANG:5;
then  H1 is negative by Th168;
then consider p1 being ZF-formula such that
A7: H1 = 'not' p1 by ZF_LANG:5;
 H = p1 'or' p2 by A3, A5, A7, A6;
hence  H is disjunctive by ZF_LANG:6; ::_thesis: verum
end;

theorem Th175: :: ZF_LANG1:175
for H being ZF-formula
for x, y being Variable holds
( H is conditional iff H / (x,y) is conditional )
proof
let H be ZF-formula; ::_thesis: for x, y being Variable holds
( H is conditional iff H / (x,y) is conditional )
let x, y be Variable; ::_thesis: ( H is conditional iff H / (x,y) is conditional )
set G = H / (x,y);
thus  ( H is conditional implies H / (x,y) is conditional ) ::_thesis: ( H / (x,y) is conditional implies H is conditional )
proof
given H1, H2 being ZF-formula such that A1: H = H1 => H2 ; :: according to ZF_LANG:def_21 ::_thesis: H / (x,y) is conditional
 H / (x,y) = (H1 / (x,y)) => (H2 / (x,y)) by A1, Th162;
hence  H / (x,y) is conditional by ZF_LANG:6; ::_thesis: verum
end;
given G1, G2 being ZF-formula such that A2: H / (x,y) = G1 => G2 ; :: according to ZF_LANG:def_21 ::_thesis: H is conditional
 H / (x,y) is negative by A2, ZF_LANG:5;
then  H is negative by Th168;
then consider H9 being ZF-formula such that
A3: H = 'not' H9 by ZF_LANG:5;
A4: G1 '&' ('not' G2) = H9 / (x,y) by A2, A3, Th156;
then  H9 / (x,y) is conjunctive by ZF_LANG:5;
then  H9 is conjunctive by Th169;
then consider H1, H2 being ZF-formula such that
A5: H9 = H1 '&' H2 by ZF_LANG:5;
 'not' G2 = H2 / (x,y) by A4, A5, Th158;
then  H2 / (x,y) is negative by ZF_LANG:5;
then  H2 is negative by Th168;
then consider p2 being ZF-formula such that
A6: H2 = 'not' p2 by ZF_LANG:5;
 H = H1 => p2 by A3, A5, A6;
hence  H is conditional by ZF_LANG:6; ::_thesis: verum
end;

theorem Th176: :: ZF_LANG1:176
for H being ZF-formula
for x, y being Variable st H is biconditional holds
H / (x,y) is biconditional
proof
let H be ZF-formula; ::_thesis: for x, y being Variable st H is biconditional holds
H / (x,y) is biconditional
let x, y be Variable; ::_thesis: ( H is biconditional implies H / (x,y) is biconditional )
given H1, H2 being ZF-formula such that A1: H = H1 <=> H2 ; :: according to ZF_LANG:def_22 ::_thesis: H / (x,y) is biconditional
 H / (x,y) = (H1 / (x,y)) <=> (H2 / (x,y)) by A1, Th163;
hence  H / (x,y) is biconditional by ZF_LANG:6; ::_thesis: verum
end;

theorem Th177: :: ZF_LANG1:177
for H being ZF-formula
for x, y being Variable holds
( H is existential iff H / (x,y) is existential )
proof
let H be ZF-formula; ::_thesis: for x, y being Variable holds
( H is existential iff H / (x,y) is existential )
let x, y be Variable; ::_thesis: ( H is existential iff H / (x,y) is existential )
thus  ( H is existential implies H / (x,y) is existential ) ::_thesis: ( H / (x,y) is existential implies H is existential )
proof
given z being Variable, H1 being ZF-formula such that A1: H = Ex (z,H1) ; :: according to ZF_LANG:def_23 ::_thesis: H / (x,y) is existential
 ( z = x or z <> x ) ;
then consider s being Variable such that
A2: ( ( z = x & s = y ) or ( z <> x & s = z ) ) ;
 H / (x,y) = Ex (s,(H1 / (x,y))) by A1, A2, Th164, Th165;
hence  H / (x,y) is existential by ZF_LANG:6; ::_thesis: verum
end;
given z being Variable, G being ZF-formula such that A3: H / (x,y) = Ex (z,G) ; :: according to ZF_LANG:def_23 ::_thesis: H is existential
 H / (x,y) is negative by A3, ZF_LANG:5;
then  H is negative by Th168;
then consider H1 being ZF-formula such that
A4: H = 'not' H1 by ZF_LANG:5;
 ( bound_in H1 = x or bound_in H1 <> x ) ;
then consider s being Variable such that
A5: ( ( bound_in H1 = x & s = y ) or ( bound_in H1 <> x & s = bound_in H1 ) ) ;
A6: H1 / (x,y) = All (z,('not' G)) by A3, A4, Th156;
then  H1 / (x,y) is universal by ZF_LANG:5;
then  H1 is universal by Th170;
then A7: H1 = All ((bound_in H1),(the_scope_of H1)) by ZF_LANG:44;
then  All (z,('not' G)) = All (s,((the_scope_of H1) / (x,y))) by A6, A5, Th159, Th160;
then  'not' G = (the_scope_of H1) / (x,y) by ZF_LANG:3;
then  (the_scope_of H1) / (x,y) is negative by ZF_LANG:5;
then  the_scope_of H1 is negative by Th168;
then  H = Ex ((bound_in H1),(the_argument_of (the_scope_of H1))) by A4, A7, ZF_LANG:def_30;
hence  H is existential by ZF_LANG:6; ::_thesis: verum
end;

theorem :: ZF_LANG1:178
for H being ZF-formula
for x, y being Variable st H is disjunctive holds
( the_left_argument_of (H / (x,y)) = (the_left_argument_of H) / (x,y) & the_right_argument_of (H / (x,y)) = (the_right_argument_of H) / (x,y) )
proof
let H be ZF-formula; ::_thesis: 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) )
let x, y be Variable; ::_thesis: ( H is disjunctive implies ( 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) ) )
assume A1: H is disjunctive ; ::_thesis: ( 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) )
then  H / (x,y) is disjunctive by Th174;
then A2: H / (x,y) = (the_left_argument_of (H / (x,y))) 'or' (the_right_argument_of (H / (x,y))) by ZF_LANG:41;
 H = (the_left_argument_of H) 'or' (the_right_argument_of H) by A1, ZF_LANG:41;
hence  ( 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) ) by A2, Th161; ::_thesis: verum
end;

theorem :: ZF_LANG1:179
for H being ZF-formula
for x, y being Variable st H is conditional holds
( the_antecedent_of (H / (x,y)) = (the_antecedent_of H) / (x,y) & the_consequent_of (H / (x,y)) = (the_consequent_of H) / (x,y) )
proof
let H be ZF-formula; ::_thesis: 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) )
let x, y be Variable; ::_thesis: ( H is conditional implies ( the_antecedent_of (H / (x,y)) = (the_antecedent_of H) / (x,y) & the_consequent_of (H / (x,y)) = (the_consequent_of H) / (x,y) ) )
assume A1: H is conditional ; ::_thesis: ( the_antecedent_of (H / (x,y)) = (the_antecedent_of H) / (x,y) & the_consequent_of (H / (x,y)) = (the_consequent_of H) / (x,y) )
then  H / (x,y) is conditional by Th175;
then A2: H / (x,y) = (the_antecedent_of (H / (x,y))) => (the_consequent_of (H / (x,y))) by ZF_LANG:47;
 H = (the_antecedent_of H) => (the_consequent_of H) by A1, ZF_LANG:47;
hence  ( the_antecedent_of (H / (x,y)) = (the_antecedent_of H) / (x,y) & the_consequent_of (H / (x,y)) = (the_consequent_of H) / (x,y) ) by A2, Th162; ::_thesis: verum
end;

theorem :: ZF_LANG1:180
for H being ZF-formula
for x, y being Variable st H is biconditional holds
( the_left_side_of (H / (x,y)) = (the_left_side_of H) / (x,y) & the_right_side_of (H / (x,y)) = (the_right_side_of H) / (x,y) )
proof
let H be ZF-formula; ::_thesis: 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) )
let x, y be Variable; ::_thesis: ( H is biconditional implies ( 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) ) )
assume  H is biconditional ; ::_thesis: ( 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) )
then  ( H = (the_left_side_of H) <=> (the_right_side_of H) & H / (x,y) = (the_left_side_of (H / (x,y))) <=> (the_right_side_of (H / (x,y))) ) by Th176, ZF_LANG:49;
hence  ( 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) ) by Th163; ::_thesis: verum
end;

theorem :: ZF_LANG1:181
for H being ZF-formula
for x, y being Variable st H is existential holds
( the_scope_of (H / (x,y)) = (the_scope_of H) / (x,y) & ( bound_in H = x implies bound_in (H / (x,y)) = y ) & ( bound_in H <> x implies bound_in (H / (x,y)) = bound_in H ) )
proof
let H be ZF-formula; ::_thesis: 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 ) )
let x, y be Variable; ::_thesis: ( H is existential implies ( 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 ) ) )
assume A1: H is existential ; ::_thesis: ( 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 ) )
then  H / (x,y) is existential by Th177;
then A2: H / (x,y) = Ex ((bound_in (H / (x,y))),(the_scope_of (H / (x,y)))) by ZF_LANG:45;
A3: H = Ex ((bound_in H),(the_scope_of H)) by A1, ZF_LANG:45;
then A4: ( bound_in H <> x implies H / (x,y) = Ex ((bound_in H),((the_scope_of H) / (x,y))) ) by Th164;
 ( bound_in H = x implies H / (x,y) = Ex (y,((the_scope_of H) / (x,y))) ) by A3, Th165;
hence  ( 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 ) ) by A2, A4, ZF_LANG:34; ::_thesis: verum
end;

theorem Th182: :: ZF_LANG1:182
for H being ZF-formula
for x, y being Variable st not x in variables_in H holds
H / (x,y) = H
proof
let H be ZF-formula; ::_thesis: for x, y being Variable st not x in variables_in H holds
H / (x,y) = H
let x, y be Variable; ::_thesis: ( not x in variables_in H implies H / (x,y) = H )
assume A1: not x in variables_in H ; ::_thesis: H / (x,y) = H
A2: not x in {0,1,2,3,4} by Th136;
A3: now__::_thesis:_for_a_being_set_st_a_in_dom_H_holds_
(H_/_(x,y))_._a_=_H_._a
let a be set ; ::_thesis: ( a in dom H implies (H / (x,y)) . a = H . a )
assume A4: a in dom H ; ::_thesis: (H / (x,y)) . a = H . a
then A5: H . a in rng H by FUNCT_1:def_3;
 ( H . a <> x implies (H / (x,y)) . a = H . a ) by A4, Def3;
hence  (H / (x,y)) . a = H . a by A1, A2, A5, XBOOLE_0:def_5; ::_thesis: verum
end;
 dom H = dom (H / (x,y)) by Def3;
hence  H / (x,y) = H by A3, FUNCT_1:2; ::_thesis: verum
end;

theorem :: ZF_LANG1:183
for H being ZF-formula
for x being Variable holds H / (x,x) = H
proof
let H be ZF-formula; ::_thesis: for x being Variable holds H / (x,x) = H
let x be Variable; ::_thesis: H / (x,x) = H
A1: now__::_thesis:_for_a_being_set_st_a_in_dom_H_holds_
H_._a_=_(H_/_(x,x))_._a
let a be set ; ::_thesis: ( a in dom H implies H . a = (H / (x,x)) . a )
assume A2: a in dom H ; ::_thesis: H . a = (H / (x,x)) . a
then  ( H . a = x implies (H / (x,x)) . a = x ) by Def3;
hence  H . a = (H / (x,x)) . a by A2, Def3; ::_thesis: verum
end;
 dom (H / (x,x)) = dom H by Def3;
hence  H / (x,x) = H by A1, FUNCT_1:2; ::_thesis: verum
end;

theorem Th184: :: ZF_LANG1:184
for H being ZF-formula
for x, y being Variable st x <> y holds
not x in variables_in (H / (x,y))
proof
let H be ZF-formula; ::_thesis: for x, y being Variable st x <> y holds
not x in variables_in (H / (x,y))
let x, y be Variable; ::_thesis: ( x <> y implies not x in variables_in (H / (x,y)) )
assume A1: x <> y ; ::_thesis: not x in variables_in (H / (x,y))
assume  x in variables_in (H / (x,y)) ; ::_thesis: contradiction
then consider a being set  such that
A2: a in dom (H / (x,y)) and
A3: x = (H / (x,y)) . a by FUNCT_1:def_3;
A4: dom (H / (x,y)) = dom H by Def3;
then  ( H . a = x implies (H / (x,y)) . a = y ) by A2, Def3;
hence  contradiction by A1, A2, A3, A4, Def3; ::_thesis: verum
end;

theorem :: ZF_LANG1:185
for H being ZF-formula
for x, y being Variable st x in variables_in H holds
y in variables_in (H / (x,y))
proof
let H be ZF-formula; ::_thesis: for x, y being Variable st x in variables_in H holds
y in variables_in (H / (x,y))
let x, y be Variable; ::_thesis: ( x in variables_in H implies y in variables_in (H / (x,y)) )
assume  x in variables_in H ; ::_thesis: y in variables_in (H / (x,y))
then consider a being set  such that
A1: a in dom H and
A2: x = H . a by FUNCT_1:def_3;
A3: dom (H / (x,y)) = dom H by Def3;
A4: not y in {0,1,2,3,4} by Th136;
 (H / (x,y)) . a = y by A1, A2, Def3;
then  y in rng (H / (x,y)) by A1, A3, FUNCT_1:def_3;
hence  y in variables_in (H / (x,y)) by A4, XBOOLE_0:def_5; ::_thesis: verum
end;

theorem :: ZF_LANG1:186
for H being ZF-formula
for x, y, z being Variable st x <> y holds
(H / (x,y)) / (x,z) = H / (x,y)
proof
let H be ZF-formula; ::_thesis: for x, y, z being Variable st x <> y holds
(H / (x,y)) / (x,z) = H / (x,y)
let x, y, z be Variable; ::_thesis: ( x <> y implies (H / (x,y)) / (x,z) = H / (x,y) )
assume  x <> y ; ::_thesis: (H / (x,y)) / (x,z) = H / (x,y)
then  not x in variables_in (H / (x,y)) by Th184;
hence  (H / (x,y)) / (x,z) = H / (x,y) by Th182; ::_thesis: verum
end;

theorem :: ZF_LANG1:187
for H being ZF-formula
for x, y being Variable holds variables_in (H / (x,y)) c= ((variables_in H) \ {x}) \/ {y}
proof
let H be ZF-formula; ::_thesis: for x, y being Variable holds variables_in (H / (x,y)) c= ((variables_in H) \ {x}) \/ {y}
let x, y be Variable; ::_thesis: variables_in (H / (x,y)) c= ((variables_in H) \ {x}) \/ {y}
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in variables_in (H / (x,y)) or a in ((variables_in H) \ {x}) \/ {y} )
assume A1: a in variables_in (H / (x,y)) ; ::_thesis: a in ((variables_in H) \ {x}) \/ {y}
then reconsider z = a as Variable ;
consider b being set  such that
A2: b in dom (H / (x,y)) and
A3: z = (H / (x,y)) . b by A1, FUNCT_1:def_3;
A4: dom (H / (x,y)) = dom H by Def3;
then A5: ( H . b <> x implies z = H . b ) by A2, A3, Def3;
 ( H . b = x implies z = y ) by A2, A3, A4, Def3;
then  ( z in {y} or ( z in rng H & not z in {0,1,2,3,4} & not z in {x} ) ) by A2, A4, A5, Th136, FUNCT_1:def_3, TARSKI:def_1;
then  ( z in {y} or ( z in (rng H) \ {0,1,2,3,4} & not z in {x} ) ) by XBOOLE_0:def_5;
then  ( z in {y} or z in (variables_in H) \ {x} ) by XBOOLE_0:def_5;
hence  a in ((variables_in H) \ {x}) \/ {y} by XBOOLE_0:def_3; ::_thesis: verum
end;