theorem :: ZFMISC_1:12

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