elsymrels3

Description: Element of the class of symmetric relations. (Contributed by Peter Mazsa, 17-Aug-2021)

		Ref	Expression
	Assertion	elsymrels3	$⊢ R \in SymRels \leftrightarrow (\forall x \forall y (x R y \to y R x) \land R \in Rels)$

Step	Hyp	Ref	Expression
1		dfsymrels3	$⊢ SymRels = \{r \in Rels \| \forall x \forall y (x r y \to y r x)\}$
2		breq	$⊢ r = R \to (x r y \leftrightarrow x R y)$
3		breq	$⊢ r = R \to (y r x \leftrightarrow y R x)$
4	2 3	imbi12d	$⊢ r = R \to ((x r y \to y r x) \leftrightarrow (x R y \to y R x))$
5	4	2albidv	$⊢ r = R \to (\forall x \forall y (x r y \to y r x) \leftrightarrow \forall x \forall y (x R y \to y R x))$
6	1 5	rabeqel	$⊢ R \in SymRels \leftrightarrow (\forall x \forall y (x R y \to y R x) \land R \in Rels)$

Metamath Proof Explorer