This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }
2	1	relopabi	⊢ Rel { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 }