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 A1: {{x,y},{x}} = {z} by TARSKI:def 5;
then {x} in {z} by TARSKI:def 2;
hence A2: z = {x} by TARSKI:def 1; :: thesis: x = y
{x,y} in {z} by A1, TARSKI:def 2;
then {x,y} = z by TARSKI:def 1;
hence x = y by A2, ZFMISC_1:5; :: thesis: verum