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 ⊢ A ∈ V
brsingle.2 ⊢ B ∈ V
Assertion brsingle ⊢ A 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 B ↔ B = A

Proof

Step Hyp Ref Expression
1 brsingle.1 ⊢ A ∈ V
2 brsingle.2 ⊢ B ∈ V
3 df-singleton ⊢ 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 = V × V ∖ ran ⁡ V ⊗ E ∆ I ⊗ V
4 brxp ⊢ A V × V B ↔ A ∈ V ∧ B ∈ V
5 1 2 4 mpbir2an ⊢ A V × V B
6 velsn ⊢ x ∈ A ↔ x = A
7 1 ideq ⊢ x I A ↔ x = A
8 6 7 bitr4i ⊢ x ∈ A ↔ x I A
9 1 2 3 5 8 brtxpsd3 ⊢ A 𝖲𝗂𝗇𝗀𝗅𝖾𝗍𝗈𝗇 B ↔ B = A