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 𝑅 → dom 𝑅 = ran 𝑅 )

Step	Hyp	Ref	Expression
1		eqvrelsymrel	⊢ ( EqvRel 𝑅 → SymRel 𝑅 )
2		symrelim	⊢ ( SymRel 𝑅 → dom 𝑅 = ran 𝑅 )
3	1 2	syl	⊢ ( EqvRel 𝑅 → dom 𝑅 = ran 𝑅 )