Description: Move class substitution in and out of class abstractions of nested ordered pairs. (Contributed by ML, 25-Oct-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | csboprabg | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | csbab | |
|
2 | sbcex2 | |
|
3 | sbcex2 | |
|
4 | sbcex2 | |
|
5 | sbcan | |
|
6 | sbcg | |
|
7 | 6 | anbi1d | |
8 | 5 7 | syl5bb | |
9 | 8 | exbidv | |
10 | 4 9 | syl5bb | |
11 | 10 | exbidv | |
12 | 3 11 | syl5bb | |
13 | 12 | exbidv | |
14 | 2 13 | syl5bb | |
15 | 14 | abbidv | |
16 | 1 15 | eqtrid | |
17 | df-oprab | |
|
18 | 17 | csbeq2i | |
19 | df-oprab | |
|
20 | 16 18 19 | 3eqtr4g | |