let y be set ; :: according to ZFMISC_1:def 10 :: thesis: for y being set st y in {x} & y in {x} holds
y = y
let z be set ; :: thesis: ( y in {x} & z in {x} implies y = z )
assume ( y in {x} & z in {x} ) ; :: thesis: y = z
then ( y = x & z = x ) by TARSKI:def 1;
hence y = z ; :: thesis: verum