Description: Alternative definition of the converse of a relation. (Contributed by Thierry Arnoux, 31-Mar-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | dfcnv2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | relcnv | |
|
2 | relxp | |
|
3 | 2 | rgenw | |
4 | reliun | |
|
5 | 3 4 | mpbir | |
6 | vex | |
|
7 | vex | |
|
8 | 6 7 | opeldm | |
9 | df-rn | |
|
10 | 8 9 | eleqtrrdi | |
11 | ssel2 | |
|
12 | 10 11 | sylan2 | |
13 | 12 | ex | |
14 | 13 | pm4.71rd | |
15 | 6 7 | elimasn | |
16 | 15 | anbi2i | |
17 | 14 16 | bitr4di | |
18 | sneq | |
|
19 | 18 | imaeq2d | |
20 | 19 | opeliunxp2 | |
21 | 17 20 | bitr4di | |
22 | 1 5 21 | eqrelrdv | |