let x, y, z be set ; :: thesis: ( [x,y] = {z} implies ( z = {x} & x = y ) )
assume [x,y] = {z} ; :: thesis: ( z = {x} & x = y )
then {{x,y},{x}} = {z} by TARSKI:def 5;
then A1: ( {x,y} in {z} & {x} in {z} ) by TARSKI:def 2;
hence A2: z = {x} by TARSKI:def 1; :: thesis: x = y
{x,y} = z by A1, TARSKI:def 1;
hence x = y by A2, ZFMISC_1:9; :: thesis: verum