:: deftheorem Def4 defines ZF-axioms ZFREFLE1:def 4 :
for b₁ being set holds
( b₁ = ZF-axioms iff for e being object holds
( e in b₁ iff ( e in WFF & ( e = the_axiom_of_extensionality or e = the_axiom_of_pairs or e = the_axiom_of_unions or e = the_axiom_of_infinity or e = the_axiom_of_power_sets or ex H being ZF-formula st
( {(x. 0),(x. 1),(x. 2)} misses Free H & e = the_axiom_of_substitution_for H ) ) ) ) );