elcnvrefrelsrel

Description: For sets, being an element of the class of converse reflexive relations ( df-cnvrefrels ) is equivalent to satisfying the converse reflexive relation predicate. (Contributed by Peter Mazsa, 25-Jul-2021)

		Ref	Expression
	Assertion	elcnvrefrelsrel	$⊢ R \in V \to (R \in CnvRefRels \leftrightarrow CnvRefRel R)$

Proof

Step	Hyp	Ref	Expression
1		elrelsrel	$⊢ R \in V \to (R \in Rels \leftrightarrow Rel R)$
2	1	anbi2d	$⊢ R \in V \to ((R \subseteq I \cap (dom R \times ran R) \land R \in Rels) \leftrightarrow (R \subseteq I \cap (dom R \times ran R) \land Rel R))$
3		elcnvrefrels2	$⊢ R \in CnvRefRels \leftrightarrow (R \subseteq I \cap (dom R \times ran R) \land R \in Rels)$
4		dfcnvrefrel2	$⊢ CnvRefRel R \leftrightarrow (R \subseteq I \cap (dom R \times ran R) \land Rel R)$
5	2 3 4	3bitr4g	$⊢ R \in V \to (R \in CnvRefRels \leftrightarrow CnvRefRel R)$

Metamath Proof Explorer

Theorem elcnvrefrelsrel

Proof