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