Theorem elrelscnveq

Description: Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 22-Aug-2021)

	Ref	Expression
Assertion	elrelscnveq	$$⊢R\in \mathrm{Rels}\to \left(R^{-1}\subseteq R\leftrightarrow R^{-1}=R\right)$$

Proof

Step	Hyp	Ref	Expression
1		elrelscnveq3	$$⊢R\in \mathrm{Rels}\to \left(R=R^{-1}\leftrightarrow \forall x\forall y\left(xRy\to yRx\right)\right)$$
2		cnvsym	$$⊢R^{-1}\subseteq R\leftrightarrow \forall x\forall y\left(xRy\to yRx\right)$$
3	1 2	bitr4di	$$⊢R\in \mathrm{Rels}\to \left(R=R^{-1}\leftrightarrow R^{-1}\subseteq R\right)$$
4		eqcom	$$⊢R=R^{-1}\leftrightarrow R^{-1}=R$$
5	3 4	bitr3di	$$⊢R\in \mathrm{Rels}\to \left(R^{-1}\subseteq R\leftrightarrow R^{-1}=R\right)$$