Description: Class abstraction restricted to a Cartesian product as an ordered-pair class abstraction. (Contributed by NM, 20-Feb-2014)
Ref | Expression | ||
---|---|---|---|
Hypothesis | rabxp.1 | |
|
Assertion | rabxp | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rabxp.1 | |
|
2 | elxp | |
|
3 | 2 | anbi1i | |
4 | 19.41vv | |
|
5 | anass | |
|
6 | 1 | anbi2d | |
7 | df-3an | |
|
8 | 6 7 | bitr4di | |
9 | 8 | pm5.32i | |
10 | 5 9 | bitri | |
11 | 10 | 2exbii | |
12 | 3 4 11 | 3bitr2i | |
13 | 12 | abbii | |
14 | df-rab | |
|
15 | df-opab | |
|
16 | 13 14 15 | 3eqtr4i | |