Metamath Proof Explorer

Theorem dfrefrels3

Description: Alternate definition of the class of reflexive relations. (Contributed by Peter Mazsa, 8-Jul-2019)

		Ref	Expression
	Assertion	dfrefrels3	$⊢ RefRels = \{r \in Rels \| \forall x \in dom r \forall y \in ran r (x = y \to x r y)\}$

Step	Hyp	Ref	Expression
1		dfrefrels2	$⊢ RefRels = \{r \in Rels \| I \cap (dom r \times ran r) \subseteq r\}$
2		idinxpss	$⊢ I \cap (dom r \times ran r) \subseteq r \leftrightarrow \forall x \in dom r \forall y \in ran r (x = y \to x r y)$
3	1 2	rabbieq	$⊢ RefRels = \{r \in Rels \| \forall x \in dom r \forall y \in ran r (x = y \to x r y)\}$