begin
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,
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 )
theorem
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 )
theorem Th17:
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 )
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,
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 )
theorem
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 )
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, ZF_LANG:5;
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, ZF_LANG:6;
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, 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)
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
::