Metamath Proof Explorer


Theorem dfcnv2

Description: Alternative definition of the converse of a relation. (Contributed by Thierry Arnoux, 31-Mar-2018)

Ref Expression
Assertion dfcnv2 ranRAR-1=xAx×R-1x

Proof

Step Hyp Ref Expression
1 relcnv RelR-1
2 relxp Relx×R-1x
3 2 rgenw xARelx×R-1x
4 reliun RelxAx×R-1xxARelx×R-1x
5 3 4 mpbir RelxAx×R-1x
6 vex zV
7 vex yV
8 6 7 opeldm zyR-1zdomR-1
9 df-rn ranR=domR-1
10 8 9 eleqtrrdi zyR-1zranR
11 ssel2 ranRAzranRzA
12 10 11 sylan2 ranRAzyR-1zA
13 12 ex ranRAzyR-1zA
14 13 pm4.71rd ranRAzyR-1zAzyR-1
15 6 7 elimasn yR-1zzyR-1
16 15 anbi2i zAyR-1zzAzyR-1
17 14 16 bitr4di ranRAzyR-1zAyR-1z
18 sneq x=zx=z
19 18 imaeq2d x=zR-1x=R-1z
20 19 opeliunxp2 zyxAx×R-1xzAyR-1z
21 17 20 bitr4di ranRAzyR-1zyxAx×R-1x
22 1 5 21 eqrelrdv ranRAR-1=xAx×R-1x