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	⊢ ( 𝐴 ∈ 𝑉 → ( Rel { 𝐴 } ↔ dom { 𝐴 } ≠ ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		relsng	⊢ ( 𝐴 ∈ 𝑉 → ( Rel { 𝐴 } ↔ 𝐴 ∈ ( V × V ) ) )
2		dmsnn0	⊢ ( 𝐴 ∈ ( V × V ) ↔ dom { 𝐴 } ≠ ∅ )
3	1 2	bitrdi	⊢ ( 𝐴 ∈ 𝑉 → ( Rel { 𝐴 } ↔ dom { 𝐴 } ≠ ∅ ) )