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	$$⊢A\in \mathrm{V}$$
	relsnop.2	$$⊢B\in \mathrm{V}$$
Assertion	relsnop	$$⊢\mathrm{Rel}\left\{⟨A,B⟩\right\}$$

Proof

Step	Hyp	Ref	Expression
1		relsn.1	$$⊢A\in \mathrm{V}$$
2		relsnop.2	$$⊢B\in \mathrm{V}$$
3		relsnopg	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)\to \mathrm{Rel}\left\{⟨A,B⟩\right\}$$
4	1 2 3	mp2an	$$⊢\mathrm{Rel}\left\{⟨A,B⟩\right\}$$