Theorem elsymrels4

Description: Element of the class of symmetric relations. (Contributed by Peter Mazsa, 17-Aug-2021)

	Ref	Expression
Assertion	elsymrels4	$$⊢R\in \mathrm{SymRels}\leftrightarrow \left(R^{-1}=R\wedge R\in \mathrm{Rels}\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfsymrels4	$$⊢\mathrm{SymRels}=\left\{r\in \mathrm{Rels}|r^{-1}=r\right\}$$
2		cnveq	$$⊢r=R\to r^{-1}=R^{-1}$$
3		id	$$⊢r=R\to r=R$$
4	2 3	eqeq12d	$$⊢r=R\to \left(r^{-1}=r\leftrightarrow R^{-1}=R\right)$$
5	1 4	rabeqel	$$⊢R\in \mathrm{SymRels}\leftrightarrow \left(R^{-1}=R\wedge R\in \mathrm{Rels}\right)$$