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 { 𝐴 } ≠ ∅ )