let x, y, z be object ; :: thesis: for X being set holds
( [x,y] in [:X,{z}:] iff ( x in X & y = z ) )
let X be set ; :: thesis: ( [x,y] in [:X,{z}:] iff ( x in X & y = z ) )
A1: ( y in {z} iff y = z ) by TARSKI:def 1;
hence ( [x,y] in [:X,{z}:] implies ( x in X & y = z ) ) by Lm16; :: thesis: ( x in X & y = z implies [x,y] in [:X,{z}:] )
thus ( x in X & y = z implies [x,y] in [:X,{z}:] ) by A1, Lm16; :: thesis: verum