This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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