theorem :: ZFMODEL1:3

for E being non empty set st E is epsilon-transitive holds
( E |= the_axiom_of_pairs iff for X, Y being set st X in E & Y in E holds
{X,Y} in E )