theorem :: ZFMISC_1:60

for x being object
for X being set holds
( {x} \ X = {} iff x in X ) by Lm1, XBOOLE_1:37;