:: deftheorem defines the_axiom_of_pairs ZF_MODEL:def 7 :
the_axiom_of_pairs = All ((x. 0),(x. 1),(Ex ((x. 2),(All ((x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)))))))));