:: deftheorem defines the_axiom_of_extensionality ZF_MODEL:def 6 :
the_axiom_of_extensionality = All ((x. 0),(x. 1),((All ((x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1))))) => ((x. 0) '=' (x. 1))));