Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990
Association of Mizar Users
The abstract of the Mizar article:
-
- by
- Grzegorz Bancerek
- Received August 10, 1990
- MML identifier: ZF_LANG1
- [
Mizar article,
MML identifier index
]
environ
vocabulary ZF_LANG, FUNCT_1, FINSEQ_1, BOOLE, ZF_MODEL, ARYTM_3, QC_LANG1,
RELAT_1, FINSET_1, QC_LANG3;
notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0,
NAT_1, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, FINSET_1, ZF_LANG, ZF_MODEL;
constructors ENUMSET1, NAT_1, ZF_MODEL, XREAL_0, MEMBERED, XBOOLE_0;
clusters SUBSET_1, FINSET_1, ZF_LANG, RELSET_1, XREAL_0, FINSEQ_1, ARYTM_3,
MEMBERED, ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2;
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 for set, 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) = All(z,q) implies x = z & All(y,p) = q;
theorem :: ZF_LANG1:12
Ex(x,y,p) = Ex(z,q) implies x = z & Ex(y,p) = q;
theorem :: ZF_LANG1:13
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:14
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:15
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:16
All(x1,y1,p1) = All(x2,y2,p2) implies x1 = x2 & y1 = y2 & p1 = p2;
theorem :: ZF_LANG1:17
All(x1,y1,z1,p1) = All(x2,y2,z2,p2) implies
x1 = x2 & y1 = y2 & z1 = z2 & p1 = p2;
theorem :: ZF_LANG1:18
All(x,y,z,p) = All(t,q) implies x = t & All(y,z,p) = q;
theorem :: ZF_LANG1:19
All(x,y,z,p) = All(t,s,q) implies x = t & y = s & All(z,p) = q;
theorem :: ZF_LANG1:20
Ex(x1,y1,p1) = Ex(x2,y2,p2) implies x1 = x2 & y1 = y2 & p1 = p2;
theorem :: ZF_LANG1:21
Ex(x,y,z,p) = Ex(x,Ex(y,Ex(z,p))) & Ex(x,y,z,p) = Ex(x,y,Ex(z,p));
theorem :: ZF_LANG1:22
Ex(x1,y1,z1,p1) = Ex(x2,y2,z2,p2) implies
x1 = x2 & y1 = y2 & z1 = z2 & p1 = p2;
theorem :: ZF_LANG1:23
Ex(x,y,z,p) = Ex(t,q) implies x = t & Ex(y,z,p) = q;
theorem :: ZF_LANG1:24
Ex(x,y,z,p) = Ex(t,s,q) implies x = t & y = s & Ex(z,p) = q;
theorem :: ZF_LANG1:25
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:26
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:27
H is disjunctive implies the_left_argument_of H =
the_argument_of the_left_argument_of the_argument_of H;
theorem :: ZF_LANG1:28
H is disjunctive implies the_right_argument_of H =
the_argument_of the_right_argument_of the_argument_of H;
theorem :: ZF_LANG1:29
H is conditional implies the_antecedent_of H =
the_left_argument_of the_argument_of H;
theorem :: ZF_LANG1:30
H is conditional implies the_consequent_of H =
the_argument_of the_right_argument_of the_argument_of H;
theorem :: ZF_LANG1:31
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:32
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:33
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:34
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:35
the_argument_of F => G = F '&' 'not' G;
theorem :: ZF_LANG1:36
the_left_argument_of F <=> G = F => G &
the_right_argument_of F <=> G = G => F;
theorem :: ZF_LANG1:37
the_argument_of Ex(x,H) = All(x,'not' H);
theorem :: ZF_LANG1:38
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:39
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:40
H is biconditional implies
H is conjunctive & the_left_argument_of H is conditional &
the_right_argument_of H is conditional;
theorem :: ZF_LANG1:41
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:42
not (H is_equality & (H is_membership or H is negative or
H is conjunctive or H is universal)) &
not (H is_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:43
F is_subformula_of G implies len F <= len G;
theorem :: ZF_LANG1:44
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;
canceled;
theorem :: ZF_LANG1:46
not H is_immediate_constituent_of H;
theorem :: ZF_LANG1:47
not (G is_proper_subformula_of H & H is_subformula_of G);
theorem :: ZF_LANG1:48
not (G is_proper_subformula_of H & H is_proper_subformula_of G);
theorem :: ZF_LANG1:49
not (G is_subformula_of H & H is_immediate_constituent_of G);
theorem :: ZF_LANG1:50
not (G is_proper_subformula_of H & H is_immediate_constituent_of G);
theorem :: ZF_LANG1:51
'not' F is_subformula_of H implies F is_proper_subformula_of H;
theorem :: ZF_LANG1:52
F '&' G is_subformula_of H implies
F is_proper_subformula_of H & G is_proper_subformula_of H;
theorem :: ZF_LANG1:53
All(x,H) is_subformula_of F implies H is_proper_subformula_of F;
theorem :: ZF_LANG1:54
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:55
'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:56
All(x,'not' H) is_proper_subformula_of Ex(x,H) &
'not' H is_proper_subformula_of Ex(x,H);
theorem :: ZF_LANG1:57
G is_subformula_of H iff G in Subformulae H;
theorem :: ZF_LANG1:58
G in Subformulae H implies Subformulae G c= Subformulae H;
theorem :: ZF_LANG1:59
H in Subformulae H;
theorem :: ZF_LANG1:60
Subformulae (F => G) =
Subformulae F \/ Subformulae G \/ { 'not' G, F '&' 'not' G, F => G };
theorem :: ZF_LANG1:61
Subformulae (F 'or' G) =
Subformulae F \/ Subformulae G \/ {'not' G, 'not' F, 'not' F '&' 'not'
G, F 'or' G};
theorem :: ZF_LANG1:62
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:63
Free (x '=' y) = {x,y};
theorem :: ZF_LANG1:64
Free (x 'in' y) = {x,y};
theorem :: ZF_LANG1:65
Free ('not' p) = Free p;
theorem :: ZF_LANG1:66
Free (p '&' q) = Free p \/ Free q;
theorem :: ZF_LANG1:67
Free All(x,p) = Free p \ {x};
theorem :: ZF_LANG1:68
Free (p 'or' q) = Free p \/ Free q;
theorem :: ZF_LANG1:69
Free (p => q) = Free p \/ Free q;
theorem :: ZF_LANG1:70
Free (p <=> q) = Free p \/ Free q;
theorem :: ZF_LANG1:71
Free Ex(x,p) = Free p \ {x};
theorem :: ZF_LANG1:72
Free All(x,y,p) = Free p \ {x,y};
theorem :: ZF_LANG1:73
Free All(x,y,z,p) = Free p \ {x,y,z};
theorem :: ZF_LANG1:74
Free Ex(x,y,p) = Free p \ {x,y};
theorem :: ZF_LANG1:75
Free Ex(x,y,z,p) = Free p \ {x,y,z};
scheme ZF_Induction { 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,E for non empty set,
e for Element of E,
m,m' for Element of M,
f,g for Function of VAR,E,
v,v' for Function of VAR,M;
definition let E,f,x,e;
func f / (x,e) -> Function of VAR,E means
:: ZF_LANG1:def 1
it.x = e & for y st it.y <> f.y holds x = y;
end;
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 2
f;
end;
canceled 2;
theorem :: ZF_LANG1:78
(v/(x,m'))/(x,m) = v/(x,m) & v/(x,v.x) = v;
theorem :: ZF_LANG1:79
x <> y implies (v/(x,m))/(y,m') = (v/(y,m'))/(x,m);
theorem :: ZF_LANG1:80
M,v |= All(x,H) iff for m holds M,v/(x,m) |= H;
theorem :: ZF_LANG1:81
M,v |= All(x,H) iff M,v/(x,m) |= All(x,H);
theorem :: ZF_LANG1:82
M,v |= Ex(x,H) iff ex m st M,v/(x,m) |= H;
theorem :: ZF_LANG1:83
M,v |= Ex(x,H) iff M,v/(x,m) |= Ex(x,H);
theorem :: ZF_LANG1:84
for v,v' st for x st x in Free H holds v'.x = v.x holds
M,v |= H implies M,v' |= H;
theorem :: ZF_LANG1:85
Free H is finite;
definition let H;
cluster Free H -> finite;
end;
reserve i,j for Nat;
theorem :: ZF_LANG1:86
x.i = x.j implies i = j;
theorem :: ZF_LANG1:87
ex i st x = x.i;
canceled;
theorem :: ZF_LANG1:89
M,v |= x '=' x;
theorem :: ZF_LANG1:90
M |= x '=' x;
theorem :: ZF_LANG1:91
not M,v |= x 'in' x;
theorem :: ZF_LANG1:92
not M |= x 'in' x & M |= 'not' x 'in' x;
theorem :: ZF_LANG1:93
M |= x '=' y iff x = y or ex a st {a} = M;
theorem :: ZF_LANG1:94
M |= 'not' x 'in' y iff x = y or for X st X in M holds X misses M;
theorem :: ZF_LANG1:95
H is_equality implies (M,v |= H iff v.Var1 H = v.Var2 H);
theorem :: ZF_LANG1:96
H is_membership implies (M,v |= H iff v.Var1 H in v.Var2 H);
theorem :: ZF_LANG1:97
H is negative implies (M,v |= H iff not M,v |= the_argument_of H);
theorem :: ZF_LANG1:98
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:99
H is universal implies
(M,v |= H iff for m holds M,v/(bound_in H,m) |= the_scope_of H);
theorem :: ZF_LANG1:100
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:101
H is conditional implies (M,v |= H iff
(M,v |= the_antecedent_of H implies M,v |= the_consequent_of H));
theorem :: ZF_LANG1:102
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:103
H is existential implies
(M,v |= H iff ex m st M,v/(bound_in H,m) |= the_scope_of H);
theorem :: ZF_LANG1:104
M |= Ex(x,H) iff for v ex m st M,v/(x,m) |= H;
theorem :: ZF_LANG1:105
M |= H implies M |= Ex(x,H);
theorem :: ZF_LANG1:106
M |= H iff M |= All(x,y,H);
theorem :: ZF_LANG1:107
M |= H implies M |= Ex(x,y,H);
theorem :: ZF_LANG1:108
M |= H iff M |= All(x,y,z,H);
theorem :: ZF_LANG1:109
M |= H implies M |= Ex(x,y,z,H);
::
:: Axioms of Logic
::
theorem :: ZF_LANG1:110
M,v |= (p <=> q) => (p => q) & M |= (p <=> q) => (p => q);
theorem :: ZF_LANG1:111
M,v |= (p <=> q) => (q => p) & M |= (p <=> q) => (q => p);
theorem :: ZF_LANG1:112
M |= (p => q) => ((q => r) => (p => r));
theorem :: ZF_LANG1:113
M,v |= p => q & M,v |= q => r implies M,v |= p => r;
theorem :: ZF_LANG1:114
M |= p => q & M |= q => r implies M |= p => r;
theorem :: ZF_LANG1:115
M,v |= (p => q) '&' (q => r) => (p => r) &
M |= (p => q) '&' (q => r) => (p => r);
theorem :: ZF_LANG1:116
M,v |= p => (q => p) & M |= p => (q => p);
theorem :: ZF_LANG1:117
M,v |= (p => (q => r)) => ((p => q) => (p => r)) &
M |= (p => (q => r)) => ((p => q) => (p => r));
theorem :: ZF_LANG1:118
M,v |= p '&' q => p & M |= p '&' q => p;
theorem :: ZF_LANG1:119
M,v |= p '&' q => q & M |= p '&' q => q;
theorem :: ZF_LANG1:120
M,v |= p '&' q => q '&' p & M |= p '&' q => q '&' p;
theorem :: ZF_LANG1:121
M,v |= p => p '&' p & M |= p => p '&' p;
theorem :: ZF_LANG1:122
M,v |= (p => q) => ((p => r) => (p => q '&' r)) &
M |= (p => q) => ((p => r) => (p => q '&' r));
theorem :: ZF_LANG1:123
M,v |= p => p 'or' q & M |= p => p 'or' q;
theorem :: ZF_LANG1:124
M,v |= q => p 'or' q & M |= q => p 'or' q;
theorem :: ZF_LANG1:125
M,v |= p 'or' q => q 'or' p & M |= p 'or' q => q 'or' p;
theorem :: ZF_LANG1:126
M,v |= p => p 'or' p & M |= p => p 'or' p;
theorem :: ZF_LANG1:127
M,v |= (p => r) => ((q => r) => (p 'or' q => r)) &
M |= (p => r) => ((q => r) => (p 'or' q => r));
theorem :: ZF_LANG1:128
M,v |= (p => r) '&' (q => r) => (p 'or' q => r) &
M |= (p => r) '&' (q => r) => (p 'or' q => r);
theorem :: ZF_LANG1:129
M,v |= (p => 'not' q) => (q => 'not' p) &
M |= (p => 'not' q) => (q => 'not' p);
theorem :: ZF_LANG1:130
M,v |= 'not' p => (p => q) & M |= 'not' p => (p => q);
theorem :: ZF_LANG1:131
M,v |= (p => q) '&' (p => 'not' q) => 'not' p & M |= (p => q) '&' (p =>
'not'
q) => 'not' p;
canceled;
theorem :: ZF_LANG1:133
M |= p => q & M |= p implies M |= q;
theorem :: ZF_LANG1:134
M,v |= 'not'(p '&' q) => 'not' p 'or' 'not' q & M |= 'not'(p '&' q) => 'not'
p 'or' 'not' q;
theorem :: ZF_LANG1:135
M,v |= 'not' p 'or' 'not' q => 'not'(p '&' q) & M |= 'not' p 'or' 'not' q =>
'not'(p '&' q);
theorem :: ZF_LANG1:136
M,v |= 'not'(p 'or' q) => 'not' p '&' 'not' q & M |= 'not'(p 'or' q) =>
'not'
p '&' 'not' q;
theorem :: ZF_LANG1:137
M,v |= 'not' p '&' 'not' q => 'not'(p 'or' q) & M |= 'not' p '&' 'not' q =>
'not'(p 'or' q);
theorem :: ZF_LANG1:138
M |= All(x,H) => H;
theorem :: ZF_LANG1:139
M |= H => Ex(x,H);
theorem :: ZF_LANG1:140
not x in Free H1 implies M |= All(x,H1 => H2) => (H1 => All(x,H2));
theorem :: ZF_LANG1:141
not x in Free H1 & M |= H1 => H2 implies M |= H1 => All(x,H2);
theorem :: ZF_LANG1:142
not x in Free H2 implies M |= All(x,H1 => H2) => (Ex(x,H1) => H2);
theorem :: ZF_LANG1:143
not x in Free H2 & M |= H1 => H2 implies M |= Ex(x,H1) => H2;
theorem :: ZF_LANG1:144
M |= H1 => All(x,H2) implies M |= H1 => H2;
theorem :: ZF_LANG1:145
M |= Ex(x,H1) => H2 implies M |= H1 => H2;
theorem :: ZF_LANG1:146
WFF c= bool [:NAT,NAT:];
::
:: Variables in ZF-formula
::
definition let H;
func variables_in H -> set equals
:: ZF_LANG1:def 3
rng H \ { 0,1,2,3,4 };
end;
canceled;
theorem :: ZF_LANG1:148
x <> 0 & x <> 1 & x <> 2 & x <> 3 & x <> 4;
theorem :: ZF_LANG1:149
not x in { 0,1,2,3,4 };
theorem :: ZF_LANG1:150
a in variables_in H implies a <> 0 & a <> 1 & a <> 2 & a <> 3 & a <> 4;
theorem :: ZF_LANG1:151
variables_in x '=' y = {x,y};
theorem :: ZF_LANG1:152
variables_in x 'in' y = {x,y};
theorem :: ZF_LANG1:153
variables_in 'not' H = variables_in H;
theorem :: ZF_LANG1:154
variables_in H1 '&' H2 = variables_in H1 \/ variables_in H2;
theorem :: ZF_LANG1:155
variables_in All(x,H) = variables_in H \/ {x};
theorem :: ZF_LANG1:156
variables_in H1 'or' H2 = variables_in H1 \/ variables_in H2;
theorem :: ZF_LANG1:157
variables_in H1 => H2 = variables_in H1 \/ variables_in H2;
theorem :: ZF_LANG1:158
variables_in H1 <=> H2 = variables_in H1 \/ variables_in H2;
theorem :: ZF_LANG1:159
variables_in Ex(x,H) = variables_in H \/ {x};
theorem :: ZF_LANG1:160
variables_in All(x,y,H) = variables_in H \/ {x,y};
theorem :: ZF_LANG1:161
variables_in Ex(x,y,H) = variables_in H \/ {x,y};
theorem :: ZF_LANG1:162
variables_in All(x,y,z,H) = variables_in H \/ {x,y,z};
theorem :: ZF_LANG1:163
variables_in Ex(x,y,z,H) = variables_in H \/ {x,y,z};
theorem :: ZF_LANG1:164
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 4
dom it = dom H & for a st a in dom H holds
(H.a = x implies it.a = y) & (H.a <> x implies it.a = H.a);
end;
canceled;
theorem :: ZF_LANG1:166
(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:167
ex z1,z2 st (x1 '=' x2)/(y1,y2) = z1 '=' z2;
theorem :: ZF_LANG1:168
(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:169
ex z1,z2 st (x1 'in' x2)/(y1,y2) = z1 'in' z2;
theorem :: ZF_LANG1:170
'not' F = ('not' H)/(x,y) iff F = H/(x,y);
theorem :: ZF_LANG1:171
H/(x,y) in WFF;
definition let H,x,y;
redefine func H/(x,y) -> ZF-formula;
end;
theorem :: ZF_LANG1:172
G1 '&' G2 = (H1 '&' H2)/(x,y) iff G1 = H1/(x,y) & G2 = H2/(x,y);
theorem :: ZF_LANG1:173
z <> x implies (All(z,G) = All(z,H)/(x,y) iff G = H/(x,y));
theorem :: ZF_LANG1:174
All(y,G) = All(x,H)/(x,y) iff G = H/(x,y);
theorem :: ZF_LANG1:175
G1 'or' G2 = (H1 'or' H2)/(x,y) iff G1 = H1/(x,y) & G2 = H2/(x,y);
theorem :: ZF_LANG1:176
G1 => G2 = (H1 => H2)/(x,y) iff G1 = H1/(x,y) & G2 = H2/(x,y);
theorem :: ZF_LANG1:177
G1 <=> G2 = (H1 <=> H2)/(x,y) iff G1 = H1/(x,y) & G2 = H2/(x,y);
theorem :: ZF_LANG1:178
z <> x implies (Ex(z,G) = Ex(z,H)/(x,y) iff G = H/(x,y));
theorem :: ZF_LANG1:179
Ex(y,G) = Ex(x,H)/(x,y) iff G = H/(x,y);
theorem :: ZF_LANG1:180
H is_equality iff H/(x,y) is_equality;
theorem :: ZF_LANG1:181
H is_membership iff H/(x,y) is_membership;
theorem :: ZF_LANG1:182
H is negative iff H/(x,y) is negative;
theorem :: ZF_LANG1:183
H is conjunctive iff H/(x,y) is conjunctive;
theorem :: ZF_LANG1:184
H is universal iff H/(x,y) is universal;
theorem :: ZF_LANG1:185
H is negative implies the_argument_of (H/(x,y)) = (the_argument_of H)/(x,y);
theorem :: ZF_LANG1:186
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:187
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:188
H is disjunctive iff H/(x,y) is disjunctive;
theorem :: ZF_LANG1:189
H is conditional iff H/(x,y) is conditional;
theorem :: ZF_LANG1:190
H is biconditional implies H/(x,y) is biconditional;
theorem :: ZF_LANG1:191
H is existential iff H/(x,y) is existential;
theorem :: ZF_LANG1:192
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:193
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:194
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:195
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:196
not x in variables_in H implies H/(x,y) = H;
theorem :: ZF_LANG1:197
H/(x,x) = H;
theorem :: ZF_LANG1:198
x <> y implies not x in variables_in (H/(x,y));
theorem :: ZF_LANG1:199
x in variables_in H implies y in variables_in (H/(x,y));
theorem :: ZF_LANG1:200
x <> y implies (H/(x,y))/(x,z) = H/(x,y);
theorem :: ZF_LANG1:201
variables_in (H/(x,y)) c= (variables_in H \ {x}) \/ {y};
Back to top