Theorem relsnop

Description: A singleton of an ordered pair is a relation. (Contributed by NM, 17-May-1998) (Revised by Mario Carneiro, 26-Apr-2015)

	Ref	Expression
Hypotheses	relsn.1	⊢ 𝐴 ∈ V
	relsnop.2	⊢ 𝐵 ∈ V
Assertion	relsnop	⊢ Rel { ⟨ 𝐴 , 𝐵 ⟩ }

Proof

Step	Hyp	Ref	Expression
1		relsn.1	⊢ 𝐴 ∈ V
2		relsnop.2	⊢ 𝐵 ∈ V
3		relsnopg	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → Rel { ⟨ 𝐴 , 𝐵 ⟩ } )
4	1 2 3	mp2an	⊢ Rel { ⟨ 𝐴 , 𝐵 ⟩ }