theorem Th55: :: ZFMISC_1:56

for x, z being object
for X being set holds
( z in X \ {x} iff ( z in X & z <> x ) )