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

Metamath Proof Explorer

Theorem rnsnn0

Description: The range of a singleton is nonzero iff the singleton argument is an ordered pair. (Contributed by NM, 14-Dec-2008)

Ref Expression
Assertion rnsnn0 ⊢ A ∈ V × V ↔ ran ⁡ A ≠ ∅

Proof

Step Hyp Ref Expression
1 dmsnn0 ⊢ A ∈ V × V ↔ dom ⁡ A ≠ ∅
2 dm0rn0 ⊢ dom ⁡ A = ∅ ↔ ran ⁡ A = ∅
3 2 necon3bii ⊢ dom ⁡ A ≠ ∅ ↔ ran ⁡ A ≠ ∅
4 1 3 bitri ⊢ A ∈ V × V ↔ ran ⁡ A ≠ ∅