let X be non empty set ; :: thesis: for x being set
for y being Element of X holds
( x in (singleton X) . y iff x = y )
let x be set ; :: thesis: for y being Element of X holds
( x in (singleton X) . y iff x = y )
let y be Element of X; :: thesis: ( x in (singleton X) . y iff x = y )
(singleton X) . y = {y} by Th51;
hence ( x in (singleton X) . y iff x = y ) by TARSKI:def 1; :: thesis: verum