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 = r Rels | x dom r y ran r x r y x = y

Proof

Step Hyp Ref Expression
1 df-cnvrefrels CnvRefRels = CnvRefs Rels
2 df-cnvrefs CnvRefs = r | I dom r × ran r S -1 r dom r × ran r
3 1 2 abeqin CnvRefRels = r Rels | I dom r × ran r S -1 r dom r × ran r
4 dmexg r V dom r V
5 4 elv dom r V
6 rnexg r V ran r V
7 6 elv ran r V
8 5 7 xpex dom r × ran r V
9 inex2g dom r × ran r V I dom r × ran r V
10 brcnvssr I dom r × ran r V I dom r × ran r S -1 r dom r × ran r r dom r × ran r I dom r × ran r
11 8 9 10 mp2b I dom r × ran r S -1 r dom r × ran r r dom r × ran r I dom r × ran r
12 inxpssidinxp r dom r × ran r I dom r × ran r x dom r y ran r x r y x = y
13 11 12 bitri I dom r × ran r S -1 r dom r × ran r x dom r y ran r x r y x = y
14 3 13 rabbieq CnvRefRels = r Rels | x dom r y ran r x r y x = y