elrefrels3

Description: Element of the class of reflexive relations. (Contributed by Peter Mazsa, 23-Jul-2019)

		Ref	Expression
	Assertion	elrefrels3	$⊢ R \in RefRels \leftrightarrow (\forall x \in dom R \forall y \in ran R (x = y \to x R y) \land R \in Rels)$

Step	Hyp	Ref	Expression
1		dfrefrels3	$⊢ RefRels = \{r \in Rels \| \forall x \in dom r \forall y \in ran r (x = y \to x r y)\}$
2		dmeq	$⊢ r = R \to dom r = dom R$
3		rneq	$⊢ r = R \to ran r = ran R$
4		breq	$⊢ r = R \to (x r y \leftrightarrow x R y)$
5	4	imbi2d	$⊢ r = R \to ((x = y \to x r y) \leftrightarrow (x = y \to x R y))$
6	3 5	raleqbidv	$⊢ r = R \to (\forall y \in ran r (x = y \to x r y) \leftrightarrow \forall y \in ran R (x = y \to x R y))$
7	2 6	raleqbidv	$⊢ r = R \to (\forall x \in dom r \forall y \in ran r (x = y \to x r y) \leftrightarrow \forall x \in dom R \forall y \in ran R (x = y \to x R y))$
8	1 7	rabeqel	$⊢ R \in RefRels \leftrightarrow (\forall x \in dom R \forall y \in ran R (x = y \to x R y) \land R \in Rels)$

Metamath Proof Explorer