environ
vocabularies HIDDEN, NUMBERS, FINSEQ_1, QC_LANG1, SUBSET_1, ZF_LANG, XBOOLEAN, XXREAL_0, CARD_1, ORDINAL4, BVFUNC_2, FUNCT_1, CLASSES2, MCART_1, REALSET1, ARYTM_3, NAT_1, RELAT_1, ARYTM_1, TARSKI, XBOOLE_0, QC_LANG2;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, XCMPLX_0, RELAT_1, FUNCT_1, ORDINAL1, NUMBERS, NAT_1, FINSEQ_1, XTUPLE_0, MCART_1, QC_LANG1, XXREAL_0;
definitions TARSKI, QC_LANG1, XBOOLE_0;
theorems TARSKI, ENUMSET1, NAT_1, FUNCT_1, FINSEQ_1, QC_LANG1, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0;
schemes NAT_1, XBOOLE_0;
registrations RELSET_1, XREAL_0, FINSEQ_1, ORDINAL1, NAT_1;
constructors HIDDEN, ENUMSET1, XXREAL_0, XREAL_0, NAT_1, QC_LANG1, XTUPLE_0, NUMBERS;
requirements HIDDEN, NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
equalities QC_LANG1;
expansions QC_LANG1;
theorem
for
A being
QC-alphabet for
x,
y,
z being
bound_QC-variable of
A for
p being
Element of
QC-WFF A holds
(
All (
x,
y,
z,
p)
= All (
x,
(All (y,z,p))) &
Ex (
x,
y,
z,
p)
= Ex (
x,
(Ex (y,z,p))) ) ;
theorem
for
A being
QC-alphabet for
p1,
p2 being
Element of
QC-WFF A for
x1,
x2,
y1,
y2,
z1,
z2 being
bound_QC-variable of
A st
All (
x1,
y1,
z1,
p1)
= All (
x2,
y2,
z2,
p2) holds
(
x1 = x2 &
y1 = y2 &
z1 = z2 &
p1 = p2 )
theorem
for
A being
QC-alphabet for
x,
y,
z being
bound_QC-variable of
A for
p,
q being
Element of
QC-WFF A for
s,
t being
bound_QC-variable of
A st
All (
x,
y,
z,
p)
= All (
t,
s,
q) holds
(
x = t &
y = s &
All (
z,
p)
= q )
theorem
for
A being
QC-alphabet for
p1,
p2 being
Element of
QC-WFF A for
x1,
x2,
y1,
y2,
z1,
z2 being
bound_QC-variable of
A st
Ex (
x1,
y1,
z1,
p1)
= Ex (
x2,
y2,
z2,
p2) holds
(
x1 = x2 &
y1 = y2 &
z1 = z2 &
p1 = p2 )
theorem
for
A being
QC-alphabet for
x,
y,
z being
bound_QC-variable of
A for
p,
q being
Element of
QC-WFF A for
s,
t being
bound_QC-variable of
A st
Ex (
x,
y,
z,
p)
= Ex (
t,
s,
q) holds
(
x = t &
y = s &
Ex (
z,
p)
= q )
theorem
for
A being
QC-alphabet for
x,
y,
z being
bound_QC-variable of
A for
p being
Element of
QC-WFF A 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 Th7;
:: Immediate constituents of QC-formulae
::