Description: The converse of a class abstraction of ordered pairs. (Contributed by NM, 11-Dec-2003) (Proof shortened by Andrew Salmon, 27-Aug-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | cnvopab |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | relcnv | ||
2 | relopab | ||
3 | vopelopabsb | ||
4 | sbcom2 | ||
5 | 3 4 | bitri | |
6 | vex | ||
7 | vex | ||
8 | 6 7 | opelcnv | |
9 | vopelopabsb | ||
10 | 5 8 9 | 3bitr4i | |
11 | 1 2 10 | eqrelriiv |