begin
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem
theorem Th6:
theorem
theorem Th8:
theorem Th9:
theorem
theorem
canceled;
theorem
canceled;
theorem
theorem
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 Th16:
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
canceled;
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 Th20:
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
canceled;
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:16;
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:22;
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th43:
theorem Th44:
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th60:
theorem
theorem
theorem Th63:
theorem Th64:
theorem Th65:
theorem Th66:
theorem Th67:
theorem
theorem Th69:
theorem
theorem Th71:
theorem Th72:
theorem
theorem Th74:
theorem
:: deftheorem ZF_LANG1:def 1 :
canceled;
:: deftheorem defines ! ZF_LANG1:def 2 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th80:
theorem Th81:
theorem Th82:
theorem
theorem
theorem Th85:
theorem
theorem
theorem
canceled;
theorem Th89:
theorem Th90:
theorem Th91:
theorem Th92:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th105:
theorem Th106:
theorem Th107:
theorem
theorem
theorem
theorem
theorem Th112:
theorem Th113:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th123:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th140:
theorem
theorem Th142:
theorem
theorem
theorem
theorem
:: deftheorem defines variables_in ZF_LANG1:def 3 :
theorem
canceled;
theorem Th148:
theorem Th149:
theorem Th150:
theorem Th151:
theorem Th152:
theorem Th153:
theorem Th154:
theorem Th155:
theorem
theorem Th157:
theorem
theorem Th159:
theorem Th160:
theorem Th161:
theorem
theorem
theorem
:: deftheorem Def4 defines / ZF_LANG1:def 4 :
theorem
canceled;
theorem Th166:
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 Th167:
theorem Th168:
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 ) ) )
theorem Th169:
theorem Th170:
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 Th171:
theorem Th172:
theorem Th173:
theorem Th174:
theorem Th175:
theorem Th176:
theorem Th177:
theorem Th178:
theorem Th179:
theorem
theorem
theorem Th182:
theorem Th183:
theorem Th184:
theorem
theorem
theorem
theorem Th188:
theorem Th189:
theorem Th190:
theorem Th191:
theorem
theorem
theorem
theorem
theorem Th196:
theorem
theorem Th198:
theorem
theorem
theorem