Description: Move class substitution in and out of an operation. (Contributed by NM, 12-Nov-2005) (Revised by NM, 23-Aug-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | csbov123 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | csbeq1 | |
|
2 | csbeq1 | |
|
3 | csbeq1 | |
|
4 | csbeq1 | |
|
5 | 2 3 4 | oveq123d | |
6 | 1 5 | eqeq12d | |
7 | vex | |
|
8 | nfcsb1v | |
|
9 | nfcsb1v | |
|
10 | nfcsb1v | |
|
11 | 8 9 10 | nfov | |
12 | csbeq1a | |
|
13 | csbeq1a | |
|
14 | csbeq1a | |
|
15 | 12 13 14 | oveq123d | |
16 | 7 11 15 | csbief | |
17 | 6 16 | vtoclg | |
18 | csbprc | |
|
19 | df-ov | |
|
20 | csbprc | |
|
21 | 20 | fveq1d | |
22 | 0fv | |
|
23 | 21 22 | eqtrdi | |
24 | 19 23 | eqtr2id | |
25 | 18 24 | eqtrd | |
26 | 17 25 | pm2.61i | |