Theorem relcnveq

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

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

Proof

Step	Hyp	Ref	Expression
1		relcnveq3	$$⊢\mathrm{Rel}R\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	$$⊢\mathrm{Rel}R\to \left(R=R^{-1}\leftrightarrow R^{-1}\subseteq R\right)$$
4		eqcom	$$⊢R=R^{-1}\leftrightarrow R^{-1}=R$$
5	3 4	bitr3di	$$⊢\mathrm{Rel}R\to \left(R^{-1}\subseteq R\leftrightarrow R^{-1}=R\right)$$