Theorem relcoss

Description: Cosets by R is a relation. (Contributed by Peter Mazsa, 27-Dec-2018)

	Ref	Expression
Assertion	relcoss	⊢ Rel ≀ 𝑅

Proof

Step	Hyp	Ref	Expression
1		df-coss	⊢ ≀ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ( 𝑢 𝑅 𝑥 ∧ 𝑢 𝑅 𝑦 ) }
2	1	relopabiv	⊢ Rel ≀ 𝑅