:: Replacing of Variables in Formulas of ZF Theory
:: by Grzegorz Bancerek
::
:: Received August 10, 1990
:: Copyright (c) 1990-2018 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, ZF_LANG, XBOOLEAN, XXREAL_0, BVFUNC_2, CLASSES2,
FUNCT_1, CARD_1, FINSEQ_1, ARYTM_3, TARSKI, XBOOLE_0, ZF_MODEL, SUBSET_1,
REALSET1, RELAT_1, FUNCT_4, FINSET_1, NAT_1, ZFMISC_1, ORDINAL4,
ZF_LANG1;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS,
XCMPLX_0, NAT_1, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, FINSET_1, ZF_LANG,
ZF_MODEL, XXREAL_0, FUNCT_7, TREES_3;
constructors ENUMSET1, XXREAL_0, XREAL_0, NAT_1, ZF_MODEL, FUNCT_7, RELSET_1,
NUMBERS, TREES_3;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FINSET_1, XXREAL_0,
NAT_1, FINSEQ_1, ZF_LANG, XCMPLX_0;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
begin
reserve p,p1,p2,q,r,F,G,G1,G2,H,H1,H2 for ZF-formula,
x,x1,x2,y,y1,y2,z,z1,z2,s,t for Variable,
a,X for set;
theorem :: ZF_LANG1:1
Var1 (x '=' y) = x & Var2 (x '=' y) = y;
theorem :: ZF_LANG1:2
Var1 (x 'in' y) = x & Var2 (x 'in' y) = y;
theorem :: ZF_LANG1:3
the_argument_of 'not' p = p;
theorem :: ZF_LANG1:4
the_left_argument_of (p '&' q) = p & the_right_argument_of (p '&' q) = q;
theorem :: ZF_LANG1:5
the_left_argument_of (p 'or' q) = p & the_right_argument_of (p 'or' q) = q;
theorem :: ZF_LANG1:6
the_antecedent_of (p => q) = p & the_consequent_of (p => q) = q;
theorem :: ZF_LANG1:7
the_left_side_of (p <=> q) = p & the_right_side_of (p <=> q) = q;
theorem :: ZF_LANG1:8
bound_in All(x,p) = x & the_scope_of All(x,p) = p;
theorem :: ZF_LANG1:9
bound_in Ex(x,p) = x & the_scope_of Ex(x,p) = p;
theorem :: ZF_LANG1:10
p 'or' q = 'not' p => q;
theorem :: ZF_LANG1:11
All(x,y,p) is universal & bound_in All(x,y,p) = x & the_scope_of All(x
,y,p) = All(y,p);
theorem :: ZF_LANG1:12
Ex(x,y,p) is existential & bound_in Ex(x,y,p) = x & the_scope_of Ex(x,
y,p) = Ex(y,p);
theorem :: ZF_LANG1:13
All(x,y,z,p) = All(x,All(y,All(z,p))) & All(x,y,z,p) = All(x,y,All(z,p ));
theorem :: ZF_LANG1:14
All(x1,y1,p1) = All(x2,y2,p2) implies x1 = x2 & y1 = y2 & p1 = p2;
theorem :: ZF_LANG1:15
All(x1,y1,z1,p1) = All(x2,y2,z2,p2) implies x1 = x2 & y1 = y2 & z1 =
z2 & p1 = p2;
theorem :: ZF_LANG1:16
All(x,y,z,p) = All(t,s,q) implies x = t & y = s & All(z,p) = q;
theorem :: ZF_LANG1:17
Ex(x1,y1,p1) = Ex(x2,y2,p2) implies x1 = x2 & y1 = y2 & p1 = p2;
theorem :: ZF_LANG1:18
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
Ex(x1,y1,z1,p1) = Ex(x2,y2,z2,p2) implies x1 = x2 & y1 = y2 & z1 = z2
& p1 = p2;
theorem :: ZF_LANG1:20
Ex(x,y,z,p) = Ex(t,s,q) implies x = t & y = s & Ex(z,p) = q;
theorem :: ZF_LANG1:21
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);
theorem :: ZF_LANG1:22
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);
theorem :: ZF_LANG1:23
H is disjunctive implies the_left_argument_of H = the_argument_of
the_left_argument_of the_argument_of H;
theorem :: ZF_LANG1:24
H is disjunctive implies the_right_argument_of H = the_argument_of
the_right_argument_of the_argument_of H;
theorem :: ZF_LANG1:25
H is conditional implies the_antecedent_of H = the_left_argument_of
the_argument_of H;
theorem :: ZF_LANG1:26
H is conditional implies the_consequent_of H = the_argument_of
the_right_argument_of the_argument_of H;
theorem :: ZF_LANG1:27
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;
theorem :: ZF_LANG1:28
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;
theorem :: ZF_LANG1:29
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;
theorem :: ZF_LANG1:30
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;
theorem :: ZF_LANG1:31
the_argument_of F => G = F '&' 'not' G;
theorem :: ZF_LANG1:32
the_left_argument_of F <=> G = F => G & the_right_argument_of F <=> G
= G => F;
theorem :: ZF_LANG1:33
the_argument_of Ex(x,H) = All(x,'not' H);
theorem :: ZF_LANG1:34
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;
theorem :: ZF_LANG1:35
H is conditional implies H is negative & the_argument_of H is
conjunctive & the_right_argument_of the_argument_of H is negative;
theorem :: ZF_LANG1:36
H is biconditional implies H is conjunctive & the_left_argument_of H
is conditional & the_right_argument_of H is conditional;
theorem :: ZF_LANG1:37
H is existential implies H is negative & the_argument_of H is
universal & the_scope_of the_argument_of H is negative;
theorem :: ZF_LANG1:38
not (H is being_equality & (H is being_membership or H is negative or
H is conjunctive or H is universal)) & not (H is being_membership & (H is
negative or H is conjunctive or H is universal)) & not (H is negative & (H is
conjunctive or H is universal)) & not (H is conjunctive & H is universal);
theorem :: ZF_LANG1:39
F is_subformula_of G implies len F <= len G;
theorem :: ZF_LANG1:40
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;
theorem :: ZF_LANG1:41
not H is_immediate_constituent_of H;
theorem :: ZF_LANG1:42
not (G is_proper_subformula_of H & H is_subformula_of G);
theorem :: ZF_LANG1:43
not (G is_proper_subformula_of H & H is_proper_subformula_of G);
theorem :: ZF_LANG1:44
not (G is_subformula_of H & H is_immediate_constituent_of G);
theorem :: ZF_LANG1:45
not (G is_proper_subformula_of H & H is_immediate_constituent_of G);
theorem :: ZF_LANG1:46
'not' F is_subformula_of H implies F is_proper_subformula_of H;
theorem :: ZF_LANG1:47
F '&' G is_subformula_of H implies F is_proper_subformula_of H & G
is_proper_subformula_of H;
theorem :: ZF_LANG1:48
All(x,H) is_subformula_of F implies H is_proper_subformula_of F;
theorem :: ZF_LANG1:49
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;
theorem :: ZF_LANG1:50
'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;
theorem :: ZF_LANG1:51
All(x,'not' H) is_proper_subformula_of Ex(x,H) & 'not' H
is_proper_subformula_of Ex(x,H);
theorem :: ZF_LANG1:52
G is_subformula_of H iff G in Subformulae H;
theorem :: ZF_LANG1:53
G in Subformulae H implies Subformulae G c= Subformulae H;
theorem :: ZF_LANG1:54
H in Subformulae H;
theorem :: ZF_LANG1:55
Subformulae (F => G) = Subformulae F \/ Subformulae G \/ { 'not'
G, F '&' 'not' G, F => G };
theorem :: ZF_LANG1:56
Subformulae (F 'or' G) = Subformulae F \/ Subformulae G \/ {'not' G,
'not' F, 'not' F '&' 'not' G, F 'or' G};
theorem :: ZF_LANG1:57
Subformulae (F <=> G) = Subformulae F \/ Subformulae G \/ { 'not' G, F
'&' 'not' G, F => G, 'not' F, G '&' 'not' F, G => F, F <=> G };
theorem :: ZF_LANG1:58
Free (x '=' y) = {x,y};
theorem :: ZF_LANG1:59
Free (x 'in' y) = {x,y};
theorem :: ZF_LANG1:60
Free ('not' p) = Free p;
theorem :: ZF_LANG1:61
Free (p '&' q) = Free p \/ Free q;
theorem :: ZF_LANG1:62
Free All(x,p) = Free p \ {x};
theorem :: ZF_LANG1:63
Free (p 'or' q) = Free p \/ Free q;
theorem :: ZF_LANG1:64
Free (p => q) = Free p \/ Free q;
theorem :: ZF_LANG1:65
Free (p <=> q) = Free p \/ Free q;
theorem :: ZF_LANG1:66
Free Ex(x,p) = Free p \ {x};
theorem :: ZF_LANG1:67
Free All(x,y,p) = Free p \ {x,y};
theorem :: ZF_LANG1:68
Free All(x,y,z,p) = Free p \ {x,y,z};
theorem :: ZF_LANG1:69
Free Ex(x,y,p) = Free p \ {x,y};
theorem :: ZF_LANG1:70
Free Ex(x,y,z,p) = Free p \ {x,y,z};
scheme :: ZF_LANG1:sch 1
ZFInduction { P[ZF-formula] } : for H holds P[H]
provided
for x1,x2 holds P[x1 '=' x2] & P[x1 'in' x2] and
for H st P[H] holds P['not' H] and
for H1,H2 st P[H1] & P[H2] holds P[H1 '&' H2] and
for H,x st P[H] holds P[All(x,H)];
reserve M for non empty set,
m,m9 for Element of M,
v,v9 for Function of VAR,M;
definition
let D,D1,D2 be non empty set, f be Function of D,D1;
assume
D1 c= D2;
func D2!f -> Function of D,D2 equals
:: ZF_LANG1:def 1
f;
end;
notation
let E be non empty set, f be Function of VAR,E, x be Variable, e be Element
of E;
synonym f / (x,e) for f+*(x,e);
end;
definition
let E be non empty set, f be Function of VAR,E, x be Variable, e be Element
of E;
redefine func f/(x,e) -> Function of VAR, E;
end;
theorem :: ZF_LANG1:71
M,v |= All(x,H) iff for m holds M,v/(x,m) |= H;
theorem :: ZF_LANG1:72
M,v |= All(x,H) iff M,v/(x,m) |= All(x,H);
theorem :: ZF_LANG1:73
M,v |= Ex(x,H) iff ex m st M,v/(x,m) |= H;
theorem :: ZF_LANG1:74
M,v |= Ex(x,H) iff M,v/(x,m) |= Ex(x,H);
theorem :: ZF_LANG1:75
for v,v9 st for x st x in Free H holds v9.x = v.x holds M,v |= H
implies M,v9 |= H;
registration
let H;
cluster Free H -> finite;
end;
reserve i,j for Element of NAT;
theorem :: ZF_LANG1:76
x.i = x.j implies i = j;
theorem :: ZF_LANG1:77
ex i st x = x.i;
theorem :: ZF_LANG1:78
M,v |= x '=' x;
theorem :: ZF_LANG1:79
M |= x '=' x;
theorem :: ZF_LANG1:80
not M,v |= x 'in' x;
theorem :: ZF_LANG1:81
not M |= x 'in' x & M |= 'not' x 'in' x;
theorem :: ZF_LANG1:82
M |= x '=' y iff x = y or ex a st {a} = M;
theorem :: ZF_LANG1:83
M |= 'not' x 'in' y iff x = y or for X st X in M holds X misses M;
theorem :: ZF_LANG1:84
H is being_equality implies (M,v |= H iff v.Var1 H = v.Var2 H);
theorem :: ZF_LANG1:85
H is being_membership implies (M,v |= H iff v.Var1 H in v.Var2 H);
theorem :: ZF_LANG1:86
H is negative implies (M,v |= H iff not M,v |= the_argument_of H);
theorem :: ZF_LANG1:87
H is conjunctive implies (M,v |= H iff M,v |= the_left_argument_of H &
M,v |= the_right_argument_of H);
theorem :: ZF_LANG1:88
H is universal implies (M,v |= H iff for m holds M,v/(bound_in H,m) |=
the_scope_of H);
theorem :: ZF_LANG1:89
H is disjunctive implies (M,v |= H iff M,v |= the_left_argument_of H
or M,v |= the_right_argument_of H);
theorem :: ZF_LANG1:90
H is conditional implies (M,v |= H iff (M,v |= the_antecedent_of H
implies M,v |= the_consequent_of H));
theorem :: ZF_LANG1:91
H is biconditional implies (M,v |= H iff (M,v |= the_left_side_of H
iff M,v |= the_right_side_of H));
theorem :: ZF_LANG1:92
H is existential implies (M,v |= H iff ex m st M,v/(bound_in H,m) |=
the_scope_of H);
theorem :: ZF_LANG1:93
M |= Ex(x,H) iff for v ex m st M,v/(x,m) |= H;
theorem :: ZF_LANG1:94
M |= H implies M |= Ex(x,H);
theorem :: ZF_LANG1:95
M |= H iff M |= All(x,y,H);
theorem :: ZF_LANG1:96
M |= H implies M |= Ex(x,y,H);
theorem :: ZF_LANG1:97
M |= H iff M |= All(x,y,z,H);
theorem :: ZF_LANG1:98
M |= H implies M |= Ex(x,y,z,H);
::
:: Axioms of Logic
::
theorem :: ZF_LANG1:99
M,v |= (p <=> q) => (p => q) & M |= (p <=> q) => (p => q);
theorem :: ZF_LANG1:100
M,v |= (p <=> q) => (q => p) & M |= (p <=> q) => (q => p);
theorem :: ZF_LANG1:101
M |= (p => q) => ((q => r) => (p => r));
theorem :: ZF_LANG1:102
M,v |= p => q & M,v |= q => r implies M,v |= p => r;
theorem :: ZF_LANG1:103
M |= p => q & M |= q => r implies M |= p => r;
theorem :: ZF_LANG1:104
M,v |= (p => q) '&' (q => r) => (p => r) & M |= (p => q) '&' (q => r)
=> (p => r);
theorem :: ZF_LANG1:105
M,v |= p => (q => p) & M |= p => (q => p);
theorem :: ZF_LANG1:106
M,v |= (p => (q => r)) => ((p => q) => (p => r)) & M |= (p => (q => r)
) => ((p => q) => (p => r));
theorem :: ZF_LANG1:107
M,v |= p '&' q => p & M |= p '&' q => p;
theorem :: ZF_LANG1:108
M,v |= p '&' q => q & M |= p '&' q => q;
theorem :: ZF_LANG1:109
M,v |= p '&' q => q '&' p & M |= p '&' q => q '&' p;
theorem :: ZF_LANG1:110
M,v |= p => p '&' p & M |= p => p '&' p;
theorem :: ZF_LANG1:111
M,v |= (p => q) => ((p => r) => (p => q '&' r)) & M |= (p => q) => ((p
=> r) => (p => q '&' r));
theorem :: ZF_LANG1:112
M,v |= p => p 'or' q & M |= p => p 'or' q;
theorem :: ZF_LANG1:113
M,v |= q => p 'or' q & M |= q => p 'or' q;
theorem :: ZF_LANG1:114
M,v |= p 'or' q => q 'or' p & M |= p 'or' q => q 'or' p;
theorem :: ZF_LANG1:115
M,v |= p => p 'or' p & M |= p => p 'or' p;
theorem :: ZF_LANG1:116
M,v |= (p => r) => ((q => r) => (p 'or' q => r)) & M |= (p => r) => ((
q => r) => (p 'or' q => r));
theorem :: ZF_LANG1:117
M,v |= (p => r) '&' (q => r) => (p 'or' q => r) & M |= (p => r) '&' (q
=> r) => (p 'or' q => r);
theorem :: ZF_LANG1:118
M,v |= (p => 'not' q) => (q => 'not' p) & M |= (p => 'not' q) => (q =>
'not' p);
theorem :: ZF_LANG1:119
M,v |= 'not' p => (p => q) & M |= 'not' p => (p => q);
theorem :: ZF_LANG1:120
M,v |= (p => q) '&' (p => 'not' q) => 'not' p & M |= (p => q) '&' (p
=> 'not' q) => 'not' p;
theorem :: ZF_LANG1:121
M |= p => q & M |= p implies M |= q;
theorem :: ZF_LANG1:122
M,v |= 'not'(p '&' q) => 'not' p 'or' 'not' q & M |= 'not'(p '&' q) =>
'not' p 'or' 'not' q;
theorem :: ZF_LANG1:123
M,v |= 'not' p 'or' 'not' q => 'not'(p '&' q) & M |= 'not' p 'or'
'not' q => 'not'(p '&' q);
theorem :: ZF_LANG1:124
M,v |= 'not'(p 'or' q) => 'not' p '&' 'not' q & M |= 'not'(p 'or' q)
=> 'not' p '&' 'not' q;
theorem :: ZF_LANG1:125
M,v |= 'not' p '&' 'not' q => 'not'(p 'or' q) & M |= 'not' p '&' 'not'
q => 'not'(p 'or' q);
theorem :: ZF_LANG1:126
M |= All(x,H) => H;
theorem :: ZF_LANG1:127
M |= H => Ex(x,H);
theorem :: ZF_LANG1:128
not x in Free H1 implies M |= All(x,H1 => H2) => (H1 => All(x, H2));
theorem :: ZF_LANG1:129
not x in Free H1 & M |= H1 => H2 implies M |= H1 => All(x,H2);
theorem :: ZF_LANG1:130
not x in Free H2 implies M |= All(x,H1 => H2) => (Ex(x,H1) => H2);
theorem :: ZF_LANG1:131
not x in Free H2 & M |= H1 => H2 implies M |= Ex(x,H1) => H2;
theorem :: ZF_LANG1:132
M |= H1 => All(x,H2) implies M |= H1 => H2;
theorem :: ZF_LANG1:133
M |= Ex(x,H1) => H2 implies M |= H1 => H2;
theorem :: ZF_LANG1:134
WFF c= bool [:NAT,NAT:];
::
:: Variables in ZF-formula
::
definition
let H;
func variables_in H -> set equals
:: ZF_LANG1:def 2
rng H \ { 0,1,2,3,4 };
end;
theorem :: ZF_LANG1:135
x <> 0 & x <> 1 & x <> 2 & x <> 3 & x <> 4;
theorem :: ZF_LANG1:136
not x in { 0,1,2,3,4 };
theorem :: ZF_LANG1:137
a in variables_in H implies a <> 0 & a <> 1 & a <> 2 & a <> 3 & a <> 4;
theorem :: ZF_LANG1:138
variables_in x '=' y = {x,y};
theorem :: ZF_LANG1:139
variables_in x 'in' y = {x,y};
theorem :: ZF_LANG1:140
variables_in 'not' H = variables_in H;
theorem :: ZF_LANG1:141
variables_in H1 '&' H2 = variables_in H1 \/ variables_in H2;
theorem :: ZF_LANG1:142
variables_in All(x,H) = variables_in H \/ {x};
theorem :: ZF_LANG1:143
variables_in H1 'or' H2 = variables_in H1 \/ variables_in H2;
theorem :: ZF_LANG1:144
variables_in H1 => H2 = variables_in H1 \/ variables_in H2;
theorem :: ZF_LANG1:145
variables_in H1 <=> H2 = variables_in H1 \/ variables_in H2;
theorem :: ZF_LANG1:146
variables_in Ex(x,H) = variables_in H \/ {x};
theorem :: ZF_LANG1:147
variables_in All(x,y,H) = variables_in H \/ {x,y};
theorem :: ZF_LANG1:148
variables_in Ex(x,y,H) = variables_in H \/ {x,y};
theorem :: ZF_LANG1:149
variables_in All(x,y,z,H) = variables_in H \/ {x,y,z};
theorem :: ZF_LANG1:150
variables_in Ex(x,y,z,H) = variables_in H \/ {x,y,z};
theorem :: ZF_LANG1:151
Free H c= variables_in H;
definition
let H;
redefine func variables_in H -> non empty Subset of VAR;
end;
definition
let H,x,y;
func H/(x,y) -> Function means
:: ZF_LANG1:def 3
dom it = dom H & for a being object st a in dom H
holds (H.a = x implies it.a = y) & (H.a <> x implies it.a = H.a);
end;
theorem :: ZF_LANG1:152
(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;
theorem :: ZF_LANG1:153
ex z1,z2 st (x1 '=' x2)/(y1,y2) = z1 '=' z2;
theorem :: ZF_LANG1:154
(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;
theorem :: ZF_LANG1:155
ex z1,z2 st (x1 'in' x2)/(y1,y2) = z1 'in' z2;
theorem :: ZF_LANG1:156
'not' F = ('not' H)/(x,y) iff F = H/(x,y);
theorem :: ZF_LANG1:157
H/(x,y) in WFF;
definition
let H,x,y;
redefine func H/(x,y) -> ZF-formula;
end;
theorem :: ZF_LANG1:158
G1 '&' G2 = (H1 '&' H2)/(x,y) iff G1 = H1/(x,y) & G2 = H2/(x,y);
theorem :: ZF_LANG1:159
z <> x implies (All(z,G) = All(z,H)/(x,y) iff G = H/(x,y));
theorem :: ZF_LANG1:160
All(y,G) = All(x,H)/(x,y) iff G = H/(x,y);
theorem :: ZF_LANG1:161
G1 'or' G2 = (H1 'or' H2)/(x,y) iff G1 = H1/(x,y) & G2 = H2/(x, y);
theorem :: ZF_LANG1:162
G1 => G2 = (H1 => H2)/(x,y) iff G1 = H1/(x,y) & G2 = H2/(x,y);
theorem :: ZF_LANG1:163
G1 <=> G2 = (H1 <=> H2)/(x,y) iff G1 = H1/(x,y) & G2 = H2/(x,y);
theorem :: ZF_LANG1:164
z <> x implies (Ex(z,G) = Ex(z,H)/(x,y) iff G = H/(x,y));
theorem :: ZF_LANG1:165
Ex(y,G) = Ex(x,H)/(x,y) iff G = H/(x,y);
theorem :: ZF_LANG1:166
H is being_equality iff H/(x,y) is being_equality;
theorem :: ZF_LANG1:167
H is being_membership iff H/(x,y) is being_membership;
theorem :: ZF_LANG1:168
H is negative iff H/(x,y) is negative;
theorem :: ZF_LANG1:169
H is conjunctive iff H/(x,y) is conjunctive;
theorem :: ZF_LANG1:170
H is universal iff H/(x,y) is universal;
theorem :: ZF_LANG1:171
H is negative implies the_argument_of (H/(x,y)) = (the_argument_of H)/
(x, y );
theorem :: ZF_LANG1:172
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);
theorem :: ZF_LANG1:173
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);
theorem :: ZF_LANG1:174
H is disjunctive iff H/(x,y) is disjunctive;
theorem :: ZF_LANG1:175
H is conditional iff H/(x,y) is conditional;
theorem :: ZF_LANG1:176
H is biconditional implies H/(x,y) is biconditional;
theorem :: ZF_LANG1:177
H is existential iff H/(x,y) is existential;
theorem :: ZF_LANG1:178
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);
theorem :: ZF_LANG1:179
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);
theorem :: ZF_LANG1:180
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);
theorem :: ZF_LANG1:181
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);
theorem :: ZF_LANG1:182
not x in variables_in H implies H/(x,y) = H;
theorem :: ZF_LANG1:183
H/(x,x) = H;
theorem :: ZF_LANG1:184
x <> y implies not x in variables_in (H/(x,y));
theorem :: ZF_LANG1:185
x in variables_in H implies y in variables_in (H/(x,y));
theorem :: ZF_LANG1:186
x <> y implies (H/(x,y))/(x,z) = H/(x,y);
theorem :: ZF_LANG1:187
variables_in (H/(x,y)) c= (variables_in H \ {x}) \/ {y};