let x, y, z, Y be set ; :: thesis: ( [x,y] in [:{z},Y:] iff ( x = z & y in Y ) )
A1: ( x in {z} iff x = z ) by TARSKI:def 1;
hence ( [x,y] in [:{z},Y:] implies ( x = z & y in Y ) ) by Lm17; :: thesis: ( x = z & y in Y implies [x,y] in [:{z},Y:] )
thus ( x = z & y in Y implies [x,y] in [:{z},Y:] ) by A1, Lm17; :: thesis: verum