Metamath Proof Explorer


Theorem relcoss

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

Ref Expression
Assertion relcoss
|- Rel ,~ R

Proof

Step Hyp Ref Expression
1 df-coss
 |-  ,~ R = { <. x , y >. | E. u ( u R x /\ u R y ) }
2 1 relopabiv
 |-  Rel ,~ R