Metamath Proof Explorer


Theorem 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 V R CnvRefRels CnvRefRel R

Proof

Step Hyp Ref Expression
1 elrelsrel R V R Rels Rel R
2 1 anbi2d R V R I dom R × ran R R Rels R I dom R × ran R Rel R
3 elcnvrefrels2 R CnvRefRels R I dom R × ran R R Rels
4 dfcnvrefrel2 CnvRefRel R R I dom R × ran R Rel R
5 2 3 4 3bitr4g R V R CnvRefRels CnvRefRel R