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