Metamath Proof Explorer

Theorem dfsymrel3

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

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

Proof

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