Metamath Proof Explorer


Theorem dfcoss4

Description: Alternate definition of the class of cosets by R (see the comment of df-coss ). (Contributed by Peter Mazsa, 12-Jul-2021)

Ref Expression
Assertion dfcoss4 R = ran R R

Proof

Step Hyp Ref Expression
1 df-coss R = x y | u u R x u R y
2 rnxrn ran R R = x y | u u R x u R y
3 1 2 eqtr4i R = ran R R