dfcnvrefrel2

Description: Alternate definition of the converse reflexive relation predicate. (Contributed by Peter Mazsa, 24-Jul-2019)

		Ref	Expression
	Assertion	dfcnvrefrel2	$⊢ CnvRefRel R \leftrightarrow (R \subseteq I \cap (dom R \times ran R) \land Rel R)$

Step	Hyp	Ref	Expression
1		df-cnvrefrel	$⊢ CnvRefRel R \leftrightarrow (R \cap (dom R \times ran R) \subseteq I \cap (dom R \times ran R) \land Rel R)$
2		dfrel6	$⊢ Rel R \leftrightarrow R \cap (dom R \times ran R) = R$
3	2	biimpi	$⊢ Rel R \to R \cap (dom R \times ran R) = R$
4	3	sseq1d	$⊢ Rel R \to (R \cap (dom R \times ran R) \subseteq I \cap (dom R \times ran R) \leftrightarrow R \subseteq I \cap (dom R \times ran R))$
5	4	pm5.32ri	$⊢ (R \cap (dom R \times ran R) \subseteq I \cap (dom R \times ran R) \land Rel R) \leftrightarrow (R \subseteq I \cap (dom R \times ran R) \land Rel R)$
6	1 5	bitri	$⊢ CnvRefRel R \leftrightarrow (R \subseteq I \cap (dom R \times ran R) \land Rel R)$

Metamath Proof Explorer