Metamath Proof Explorer


Theorem elcnvrefrels2

Description: Element of the class of converse reflexive relations. (Contributed by Peter Mazsa, 25-Jul-2019)

Ref Expression
Assertion elcnvrefrels2 R CnvRefRels R I dom R × ran R R Rels

Proof

Step Hyp Ref Expression
1 dfcnvrefrels2 CnvRefRels = r Rels | r I dom r × ran r
2 id r = R r = R
3 dmeq r = R dom r = dom R
4 rneq r = R ran r = ran R
5 3 4 xpeq12d r = R dom r × ran r = dom R × ran R
6 5 ineq2d r = R I dom r × ran r = I dom R × ran R
7 2 6 sseq12d r = R r I dom r × ran r R I dom R × ran R
8 1 7 rabeqel R CnvRefRels R I dom R × ran R R Rels