Theorem rele

Description: The membership relation is a relation. (Contributed by NM, 26-Apr-1998) (Revised by Mario Carneiro, 21-Dec-2013)

	Ref	Expression
Assertion	rele	⊢ Rel E

Proof

Step	Hyp	Ref	Expression
1		df-eprel	⊢ E = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ∈ 𝑦 }
2	1	relopabiv	⊢ Rel E