Theorem relopab

Description: A class of ordered pairs is a relation. (Contributed by NM, 8-Mar-1995) Remove disjoint variable conditions. (Revised by Alan Sare, 9-Jul-2013) (Proof shortened by Mario Carneiro, 21-Dec-2013)

	Ref	Expression
Assertion	relopab	$$⊢\mathrm{Rel}\left\{⟨x,y⟩|\phi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\left\{⟨x,y⟩|\phi \right\}=\left\{⟨x,y⟩|\phi \right\}$$
2	1	relopabi	$$⊢\mathrm{Rel}\left\{⟨x,y⟩|\phi \right\}$$