Theorem relcoss

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

	Ref	Expression
Assertion	relcoss	$$⊢\mathrm{Rel}\wr R$$

Proof

Step	Hyp	Ref	Expression
1		df-coss	$$⊢\wr R=\left\{⟨x,y⟩|\exists u\left(uRx\wedge uRy\right)\right\}$$
2	1	relopabiv	$$⊢\mathrm{Rel}\wr R$$