Theorem relsng

Description: A singleton is a relation iff it is a singleton on an ordered pair. (Contributed by NM, 24-Sep-2013) (Revised by BJ, 12-Feb-2022)

	Ref	Expression
Assertion	relsng	⊢ ( 𝐴 ∈ 𝑉 → ( Rel { 𝐴 } ↔ 𝐴 ∈ ( V × V ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-rel	⊢ ( Rel { 𝐴 } ↔ { 𝐴 } ⊆ ( V × V ) )
2		snssg	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ ( V × V ) ↔ { 𝐴 } ⊆ ( V × V ) ) )
3	1 2	bitr4id	⊢ ( 𝐴 ∈ 𝑉 → ( Rel { 𝐴 } ↔ 𝐴 ∈ ( V × V ) ) )