Description: The converse of a class abstraction of ordered pairs. (Contributed by NM, 11-Dec-2003) (Proof shortened by Andrew Salmon, 27-Aug-2011) Avoid ax-10 , ax-12 . (Revised by SN, 7-Jun-2025)
Ref | Expression | ||
---|---|---|---|
Assertion | cnvopab | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | relcnv | |
|
2 | relopabv | |
|
3 | elopab | |
|
4 | excom | |
|
5 | ancom | |
|
6 | vex | |
|
7 | vex | |
|
8 | 6 7 | opth | |
9 | 7 6 | opth | |
10 | 5 8 9 | 3bitr4i | |
11 | 10 | anbi1i | |
12 | 11 | 2exbii | |
13 | 3 4 12 | 3bitri | |
14 | 7 6 | opelcnv | |
15 | elopab | |
|
16 | 13 14 15 | 3bitr4i | |
17 | 1 2 16 | eqrelriiv | |