Theorem relcnveq4

Description: Two ways of saying a relation is symmetric. (Contributed by Peter Mazsa, 28-Apr-2019)

	Ref	Expression
Assertion	relcnveq4	$$⊢\mathrm{Rel}R\to \left(R^{-1}\subseteq R\leftrightarrow \forall x\forall y\left(xRy\leftrightarrow yRx\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		relcnveq	$$⊢\mathrm{Rel}R\to \left(R^{-1}\subseteq R\leftrightarrow R^{-1}=R\right)$$
2		relcnveq2	$$⊢\mathrm{Rel}R\to \left(R^{-1}=R\leftrightarrow \forall x\forall y\left(xRy\leftrightarrow yRx\right)\right)$$
3	1 2	bitrd	$$⊢\mathrm{Rel}R\to \left(R^{-1}\subseteq R\leftrightarrow \forall x\forall y\left(xRy\leftrightarrow yRx\right)\right)$$