Metamath Proof Explorer


Theorem dfcnvrefrels3

Description: Alternate definition of the class of converse reflexive relations. (Contributed by Peter Mazsa, 22-Jul-2019)

Ref Expression
Assertion dfcnvrefrels3 CnvRefRels=rRels|xdomryranrxryx=y

Proof

Step Hyp Ref Expression
1 df-cnvrefrels CnvRefRels=CnvRefsRels
2 df-cnvrefs CnvRefs=r|Idomr×ranrS-1rdomr×ranr
3 1 2 abeqin CnvRefRels=rRels|Idomr×ranrS-1rdomr×ranr
4 dmexg rVdomrV
5 4 elv domrV
6 rnexg rVranrV
7 6 elv ranrV
8 5 7 xpex domr×ranrV
9 inex2g domr×ranrVIdomr×ranrV
10 brcnvssr Idomr×ranrVIdomr×ranrS-1rdomr×ranrrdomr×ranrIdomr×ranr
11 8 9 10 mp2b Idomr×ranrS-1rdomr×ranrrdomr×ranrIdomr×ranr
12 inxpssidinxp rdomr×ranrIdomr×ranrxdomryranrxryx=y
13 11 12 bitri Idomr×ranrS-1rdomr×ranrxdomryranrxryx=y
14 3 13 rabbieq CnvRefRels=rRels|xdomryranrxryx=y