dfsymrel5

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

		Ref	Expression
	Assertion	dfsymrel5	$⊢ SymRel R \leftrightarrow (\forall x \forall y (x R y \leftrightarrow y R x) \land Rel R)$

Step	Hyp	Ref	Expression
1		dfsymrel2	$⊢ SymRel R \leftrightarrow (R^{-1} \subseteq R \land Rel R)$
2		relcnveq4	$⊢ Rel R \to (R^{-1} \subseteq R \leftrightarrow \forall x \forall y (x R y \leftrightarrow y R x))$
3	2	pm5.32ri	$⊢ (R^{-1} \subseteq R \land Rel R) \leftrightarrow (\forall x \forall y (x R y \leftrightarrow y R x) \land Rel R)$
4	1 3	bitri	$⊢ SymRel R \leftrightarrow (\forall x \forall y (x R y \leftrightarrow y R x) \land Rel R)$

Metamath Proof Explorer