theorem :: ZFMISC_1:62

for x, y being object
for X being set holds
( {x,y} \ X = {x} iff ( not x in X & ( y in X or x = y ) ) ) by Lm11;