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

Metamath Proof Explorer

Theorem symrelim

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

		Ref	Expression
	Assertion	symrelim	$⊢ SymRel R \to dom R = ran R$

Step	Hyp	Ref	Expression
1		rncnv	$⊢ ran R^{-1} = dom R$
2		dfsymrel4	$⊢ SymRel R \leftrightarrow (R^{-1} = R \land Rel R)$
3	2	simplbi	$⊢ SymRel R \to R^{-1} = R$
4	3	rneqd	$⊢ SymRel R \to ran R^{-1} = ran R$
5	1 4	eqtr3id	$⊢ SymRel R \to dom R = ran R$