let x, y, z be object ; :: thesis: for Y being set holds
( [x,y] in [:{z},Y:] iff ( x = z & y in Y ) )
let 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 Lm16; :: 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, Lm16; :: thesis: verum