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

Proof

Step	Hyp	Ref	Expression
1		rncnv	⊢ ran ◡ 𝑅 = dom 𝑅
2		dfsymrel4	⊢ ( SymRel 𝑅 ↔ ( ◡ 𝑅 = 𝑅 ∧ Rel 𝑅 ) )
3	2	simplbi	⊢ ( SymRel 𝑅 → ◡ 𝑅 = 𝑅 )
4	3	rneqd	⊢ ( SymRel 𝑅 → ran ◡ 𝑅 = ran 𝑅 )
5	1 4	eqtr3id	⊢ ( SymRel 𝑅 → dom 𝑅 = ran 𝑅 )