Theorem brsingle

Description: The binary relation form of the singleton function. (Contributed by Scott Fenton, 4-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Hypotheses	brsingle.1	|- A e. _V
	brsingle.2	|- B e. _V
Assertion	brsingle	|- ( A Singleton B <-> B = { A } )

Proof

Step	Hyp	Ref	Expression
1		brsingle.1	|- A e. _V
2		brsingle.2	|- B e. _V
3		df-singleton	|- Singleton = ( ( _V X. _V ) \ ran ( ( _V (x) _E ) /_\ ( _I (x) _V ) ) )
4		brxp	|- ( A ( _V X. _V ) B <-> ( A e. _V /\ B e. _V ) )
5	1 2 4	mpbir2an	|- A ( _V X. _V ) B
6		velsn	|- ( x e. { A } <-> x = A )
7	1	ideq	|- ( x _I A <-> x = A )
8	6 7	bitr4i	|- ( x e. { A } <-> x _I A )
9	1 2 3 5 8	brtxpsd3	|- ( A Singleton B <-> B = { A } )