Theorem dfsymrel4

Description: Alternate definition of the symmetric relation predicate. (Contributed by Peter Mazsa, 17-Aug-2021)

	Ref	Expression
Assertion	dfsymrel4	$$⊢SymRelR\leftrightarrow \left(R^{-1}=R\wedge \mathrm{Rel}R\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfsymrel2	$$⊢SymRelR\leftrightarrow \left(R^{-1}\subseteq R\wedge \mathrm{Rel}R\right)$$
2		relcnveq	$$⊢\mathrm{Rel}R\to \left(R^{-1}\subseteq R\leftrightarrow R^{-1}=R\right)$$
3	2	pm5.32ri	$$⊢\left(R^{-1}\subseteq R\wedge \mathrm{Rel}R\right)\leftrightarrow \left(R^{-1}=R\wedge \mathrm{Rel}R\right)$$
4	1 3	bitri	$$⊢SymRelR\leftrightarrow \left(R^{-1}=R\wedge \mathrm{Rel}R\right)$$