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 ( 𝐴 ∈ ( V × V ) ↔ dom { 𝐴 } ≠ ∅ )

Proof

Step Hyp Ref Expression
1 vex ⊢ 𝑥 ∈ V
2 1 eldm ⊢ ( 𝑥 ∈ dom { 𝐴 } ↔ ∃ 𝑦 𝑥 { 𝐴 } 𝑦 )
3 df-br ⊢ ( 𝑥 { 𝐴 } 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ { 𝐴 } )
4 opex ⊢ ⟨ 𝑥 , 𝑦 ⟩ ∈ V
5 4 elsn ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { 𝐴 } ↔ ⟨ 𝑥 , 𝑦 ⟩ = 𝐴 )
6 eqcom ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = 𝐴 ↔ 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ )
7 3 5 6 3bitri ⊢ ( 𝑥 { 𝐴 } 𝑦 ↔ 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ )
8 7 exbii ⊢ ( ∃ 𝑦 𝑥 { 𝐴 } 𝑦 ↔ ∃ 𝑦 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ )
9 2 8 bitr2i ⊢ ( ∃ 𝑦 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝑥 ∈ dom { 𝐴 } )
10 9 exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ↔ ∃ 𝑥 𝑥 ∈ dom { 𝐴 } )
11 elvv ⊢ ( 𝐴 ∈ ( V × V ) ↔ ∃ 𝑥 ∃ 𝑦 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ )
12 n0 ⊢ ( dom { 𝐴 } ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ dom { 𝐴 } )
13 10 11 12 3bitr4i ⊢ ( 𝐴 ∈ ( V × V ) ↔ dom { 𝐴 } ≠ ∅ )