Theorem dfsymrels4

Description: Alternate definition of the class of symmetric relations. (Contributed by Peter Mazsa, 20-Jul-2019)

	Ref	Expression
Assertion	dfsymrels4	$$⊢\mathrm{SymRels}=\left\{r\in \mathrm{Rels}|r^{-1}=r\right\}$$

Proof

Step	Hyp	Ref	Expression
1		dfsymrels2	$$⊢\mathrm{SymRels}=\left\{r\in \mathrm{Rels}|r^{-1}\subseteq r\right\}$$
2		elrelscnveq	$$⊢r\in \mathrm{Rels}\to \left(r^{-1}\subseteq r\leftrightarrow r^{-1}=r\right)$$
3	1 2	rabimbieq	$$⊢\mathrm{SymRels}=\left\{r\in \mathrm{Rels}|r^{-1}=r\right\}$$