elcnvrefrels3

Description: Element of the class of converse reflexive relations. (Contributed by Peter Mazsa, 30-Aug-2021)

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

Step	Hyp	Ref	Expression
1		dfcnvrefrels3	$⊢ CnvRefRels = \{r \in Rels \| \forall x \in dom r \forall y \in ran r (x r y \to x = 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	imbi1d	$⊢ r = R \to ((x r y \to x = y) \leftrightarrow (x R y \to x = y))$
6	3 5	raleqbidv	$⊢ r = R \to (\forall y \in ran r (x r y \to x = y) \leftrightarrow \forall y \in ran R (x R y \to x = y))$
7	2 6	raleqbidv	$⊢ r = R \to (\forall x \in dom r \forall y \in ran r (x r y \to x = y) \leftrightarrow \forall x \in dom R \forall y \in ran R (x R y \to x = y))$
8	1 7	rabeqel	$⊢ R \in CnvRefRels \leftrightarrow (\forall x \in dom R \forall y \in ran R (x R y \to x = y) \land R \in Rels)$

Metamath Proof Explorer