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

Metamath Proof Explorer

Theorem dmsnn0

Description: The domain of a singleton is nonzero iff the singleton argument is an ordered pair. (Contributed by NM, 14-Dec-2008) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Assertion dmsnn0 ⊢ A ∈ V × V ↔ dom ⁡ A ≠ ∅

Proof

Step Hyp Ref Expression
1 vex ⊢ x ∈ V
2 1 eldm ⊢ x ∈ dom ⁡ A ↔ ∃ y x A y
3 df-br ⊢ x A y ↔ x y ∈ A
4 opex ⊢ x y ∈ V
5 4 elsn ⊢ x y ∈ A ↔ x y = A
6 eqcom ⊢ x y = A ↔ A = x y
7 3 5 6 3bitri ⊢ x A y ↔ A = x y
8 7 exbii ⊢ ∃ y x A y ↔ ∃ y A = x y
9 2 8 bitr2i ⊢ ∃ y A = x y ↔ x ∈ dom ⁡ A
10 9 exbii ⊢ ∃ x ∃ y A = x y ↔ ∃ x x ∈ dom ⁡ A
11 elvv ⊢ A ∈ V × V ↔ ∃ x ∃ y A = x y
12 n0 ⊢ dom ⁡ A ≠ ∅ ↔ ∃ x x ∈ dom ⁡ A
13 10 11 12 3bitr4i ⊢ A ∈ V × V ↔ dom ⁡ A ≠ ∅