This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐵 ↔ 𝐵 = { 𝐴 } )