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	|- Rel { <. x , y >. | ph }

Proof

Step	Hyp	Ref	Expression
1		eqid	|- { <. x , y >. | ph } = { <. x , y >. | ph }
2	1	relopabi	|- Rel { <. x , y >. | ph }