refsymrels3

Description: Elements of the class of reflexive relations which are elements of the class of symmetric relations as well (like the elements of the class of equivalence relations dfeqvrels3 ) can use the A. x e. dom r x r x version for their reflexive part, not just the A. x e. dom r A. y e. ran r ( x = y -> x r y ) version of dfrefrels3 , cf. the comment of dfrefrel3 . (Contributed by Peter Mazsa, 22-Jul-2019) (Proof modification is discouraged.)

		Ref	Expression
	Assertion	refsymrels3	$⊢ RefRels \cap SymRels = \{r \in Rels \| (\forall x \in dom r x r x \land \forall x \forall y (x r y \to y r x))\}$

Proof

Step	Hyp	Ref	Expression
1		refsymrels2	$⊢ RefRels \cap SymRels = \{r \in Rels \| ({I ↾}_{dom r} \subseteq r \land r^{-1} \subseteq r)\}$
2		idrefALT	$⊢ {I ↾}_{dom r} \subseteq r \leftrightarrow \forall x \in dom r x r x$
3		cnvsym	$⊢ r^{-1} \subseteq r \leftrightarrow \forall x \forall y (x r y \to y r x)$
4	2 3	anbi12i	$⊢ ({I ↾}_{dom r} \subseteq r \land r^{-1} \subseteq r) \leftrightarrow (\forall x \in dom r x r x \land \forall x \forall y (x r y \to y r x))$
5	1 4	rabbieq	$⊢ RefRels \cap SymRels = \{r \in Rels \| (\forall x \in dom r x r x \land \forall x \forall y (x r y \to y r x))\}$

Metamath Proof Explorer

Theorem refsymrels3

Proof