Theorem relsnopg

Description: A singleton of an ordered pair is a relation. (Contributed by NM, 17-May-1998) (Revised by BJ, 12-Feb-2022)

	Ref	Expression
Assertion	relsnopg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → Rel { ⟨ 𝐴 , 𝐵 ⟩ } )

Proof

Step	Hyp	Ref	Expression
1		opelvvg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( V × V ) )
2		opex	⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ V
3		relsng	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ V → ( Rel { ⟨ 𝐴 , 𝐵 ⟩ } ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( V × V ) ) )
4	2 3	mp1i	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( Rel { ⟨ 𝐴 , 𝐵 ⟩ } ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( V × V ) ) )
5	1 4	mpbird	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → Rel { ⟨ 𝐴 , 𝐵 ⟩ } )