Metamath Proof Explorer


Theorem eqvrelim

Description: Equivalence relation implies that the domain and the range are equal. (Contributed by Peter Mazsa, 29-Dec-2021)

Ref Expression
Assertion eqvrelim EqvRel R dom R = ran R

Proof

Step Hyp Ref Expression
1 eqvrelsymrel EqvRel R SymRel R
2 symrelim SymRel R dom R = ran R
3 1 2 syl EqvRel R dom R = ran R