theorem :: FUNCT_4:3

for X, Y being set holds
( id X c= id Y iff X c= Y )