environ
vocabularies HIDDEN, 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 HIDDEN, 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;
definitions TARSKI, ZF_LANG, ZF_MODEL, XBOOLE_0;
theorems TARSKI, ZFMISC_1, ENUMSET1, NAT_1, FINSEQ_1, FINSEQ_3, FUNCT_1, FUNCT_2, ZF_LANG, ZF_MODEL, ZFMODEL1, RELSET_1, XBOOLE_0, XBOOLE_1, XXREAL_0, ORDINAL1, FUNCT_7, RELAT_1;
schemes PARTFUN1, ZF_LANG;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FINSET_1, XXREAL_0, NAT_1, FINSEQ_1, ZF_LANG, XCMPLX_0;
constructors HIDDEN, ENUMSET1, XXREAL_0, XREAL_0, NAT_1, ZF_MODEL, FUNCT_7, RELSET_1, NUMBERS, TREES_3;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities ZF_LANG;
expansions TARSKI, ZF_LANG, ZF_MODEL;
theorem
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
for
p1,
p2 being
ZF-formula for
x1,
x2,
y1,
y2,
z1,
z2 being
Variable st
All (
x1,
y1,
z1,
p1)
= All (
x2,
y2,
z2,
p2) holds
(
x1 = x2 &
y1 = y2 &
z1 = z2 &
p1 = p2 )
theorem
for
p,
q being
ZF-formula for
x,
y,
z,
s,
t being
Variable st
All (
x,
y,
z,
p)
= All (
t,
s,
q) holds
(
x = t &
y = s &
All (
z,
p)
= q )
theorem Th17:
for
p1,
p2 being
ZF-formula for
x1,
x2,
y1,
y2 being
Variable st
Ex (
x1,
y1,
p1)
= Ex (
x2,
y2,
p2) holds
(
x1 = x2 &
y1 = y2 &
p1 = p2 )
theorem
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
for
p1,
p2 being
ZF-formula for
x1,
x2,
y1,
y2,
z1,
z2 being
Variable st
Ex (
x1,
y1,
z1,
p1)
= Ex (
x2,
y2,
z2,
p2) holds
(
x1 = x2 &
y1 = y2 &
z1 = z2 &
p1 = p2 )
theorem
for
p,
q being
ZF-formula for
x,
y,
z,
s,
t being
Variable st
Ex (
x,
y,
z,
p)
= Ex (
t,
s,
q) holds
(
x = t &
y = s &
Ex (
z,
p)
= q )
theorem
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;
theorem
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;
theorem Th152:
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 ) ) )
theorem Th154:
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 ) ) )
Lm1:
for G1, G2, H1, 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)
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)
theorem Th162:
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) ) )
:: Axioms of Logic
::