Theorem dfcnvrefrel4

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

	Ref	Expression
Assertion	dfcnvrefrel4	$$⊢CnvRefRelR\leftrightarrow \left(R\subseteq \mathrm{I}\wedge \mathrm{Rel}R\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-cnvrefrel	$$⊢CnvRefRelR\leftrightarrow \left(R\cap \left(\mathrm{dom}R\times \mathrm{ran}R\right)\subseteq \mathrm{I}\cap \left(\mathrm{dom}R\times \mathrm{ran}R\right)\wedge \mathrm{Rel}R\right)$$
2		cnvref4	$$⊢\mathrm{Rel}R\to \left(R\cap \left(\mathrm{dom}R\times \mathrm{ran}R\right)\subseteq \mathrm{I}\cap \left(\mathrm{dom}R\times \mathrm{ran}R\right)\leftrightarrow R\subseteq \mathrm{I}\right)$$
3	1 2	bianim	$$⊢CnvRefRelR\leftrightarrow \left(R\subseteq \mathrm{I}\wedge \mathrm{Rel}R\right)$$