:: deftheorem defines the_axiom_of_unions ZF_MODEL:def 8 :
the_axiom_of_unions = All ((x. 0),(Ex ((x. 1),(All ((x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex ((x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))))))));