theorem :: ZFMISC_1:55

for x, y being object
for X being set st {x,y} /\ X = {x,y} holds
x in X