Theorem dfcnvrefrel5

Description: Alternate definition of the converse reflexive relation predicate. (Contributed by Peter Mazsa, 25-May-2024)

	Ref	Expression
Assertion	dfcnvrefrel5	$$⊢CnvRefRelR\leftrightarrow \left(\forall x\forall y\left(xRy\to x=y\right)\wedge \mathrm{Rel}R\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfcnvrefrel4	$$⊢CnvRefRelR\leftrightarrow \left(R\subseteq \mathrm{I}\wedge \mathrm{Rel}R\right)$$
2		cnvref5	$$⊢\mathrm{Rel}R\to \left(R\subseteq \mathrm{I}\leftrightarrow \forall x\forall y\left(xRy\to x=y\right)\right)$$
3	1 2	bianim	$$⊢CnvRefRelR\leftrightarrow \left(\forall x\forall y\left(xRy\to x=y\right)\wedge \mathrm{Rel}R\right)$$