theorem :: ZFMISC_1:106

for x, y, z being object
for X being set holds
( [x,y] in [:X,{z}:] iff ( x in X & y = z ) )