let x, y, z be set ; :: thesis: ( [x,y] = {z} implies ( z = {x} & x = y ) )

assume A1: [x,y] = {z} ; :: thesis: ( z = {x} & x = y )

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

assume A1: [x,y] = {z} ; :: thesis: ( z = {x} & x = y )

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