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	⊢ 𝐴 ∈ V
	brsingle.2	⊢ 𝐵 ∈ V
Assertion	brsingle	⊢ ( 𝐴 Singleton 𝐵 ↔ 𝐵 = { 𝐴 } )

Proof

Step	Hyp	Ref	Expression
1		brsingle.1	⊢ 𝐴 ∈ V
2		brsingle.2	⊢ 𝐵 ∈ V
3		df-singleton	⊢ Singleton = ( ( V × V ) ∖ ran ( ( V ⊗ E ) △ ( I ⊗ V ) ) )
4		brxp	⊢ ( 𝐴 ( V × V ) 𝐵 ↔ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
5	1 2 4	mpbir2an	⊢ 𝐴 ( V × V ) 𝐵
6		velsn	⊢ ( 𝑥 ∈ { 𝐴 } ↔ 𝑥 = 𝐴 )
7	1	ideq	⊢ ( 𝑥 I 𝐴 ↔ 𝑥 = 𝐴 )
8	6 7	bitr4i	⊢ ( 𝑥 ∈ { 𝐴 } ↔ 𝑥 I 𝐴 )
9	1 2 3 5 8	brtxpsd3	⊢ ( 𝐴 Singleton 𝐵 ↔ 𝐵 = { 𝐴 } )