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 |X. R )

Proof

Step Hyp Ref Expression
1 df-coss 
 |-  ,~ R = { <. x , y >. | E. u ( u R x /\ u R y ) }
2 rnxrn 
 |-  ran ( R |X. R ) = { <. x , y >. | E. u ( u R x /\ u R y ) }
3 1 2 eqtr4i 
 |-  ,~ R = ran ( R |X. R )