Theorem elrelscnveq4

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

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

Proof

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