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

Metamath Proof Explorer

Theorem relsn2

Description: A singleton is a relation iff it has a nonempty domain. (Contributed by NM, 25-Sep-2013) Make hypothesis an antecedent. (Revised by BJ, 12-Feb-2022)

Ref Expression
Assertion relsn2 ⊢ A ∈ V → Rel ⁡ A ↔ dom ⁡ A ≠ ∅

Proof

Step Hyp Ref Expression
1 relsng ⊢ A ∈ V → Rel ⁡ A ↔ A ∈ V × V
2 dmsnn0 ⊢ A ∈ V × V ↔ dom ⁡ A ≠ ∅
3 1 2 bitrdi ⊢ A ∈ V → Rel ⁡ A ↔ dom ⁡ A ≠ ∅