Theorem elsymrels2

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

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

Proof

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