Metamath Proof Explorer

Theorem dmcoss2

Description: The domain of cosets is the range. (Contributed by Peter Mazsa, 27-Dec-2018)

Ref Expression
Assertion dmcoss2 
|- dom ,~ R = ran R

Proof

Step Hyp Ref Expression
1 dmcoss3 
 |-  dom ,~ R = dom `' R
2 df-rn 
 |-  ran R = dom `' R
3 1 2 eqtr4i 
 |-  dom ,~ R = ran R