begin
Lm1:
{} in omega
by ORDINAL1:def 12;
Lm2:
omega is limit_ordinal
by ORDINAL1:def 12;
:: deftheorem Def1 defines |= ZFREFLE1:def 1 :
:: deftheorem defines <==> ZFREFLE1:def 2 :
:: deftheorem defines is_elementary_subsystem_of ZFREFLE1:def 3 :
defpred S1[ set ] means ( $1 = the_axiom_of_extensionality or $1 = the_axiom_of_pairs or $1 = the_axiom_of_unions or $1 = the_axiom_of_infinity or $1 = the_axiom_of_power_sets or ex H being ZF-formula st
( {(x. 0 ),(x. 1),(x. 2)} misses Free H & $1 = the_axiom_of_substitution_for H ) );
:: deftheorem Def4 defines ZF-axioms ZFREFLE1:def 4 :
theorem
theorem
theorem
theorem Th4:
theorem Th5:
theorem Th6:
theorem
theorem Th8:
theorem Th9:
theorem Th10:
theorem
canceled;
theorem Th12:
theorem
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem
canceled;
theorem
theorem
theorem
theorem Th22:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem
theorem
theorem Th40:
theorem Th41:
theorem
theorem