Description: Idempotent law for class substitutions. (Contributed by NM, 1-Mar-2008) (Revised by NM, 18-Aug-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | csbidm | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | csbnest1g | |
|
2 | csbconstg | |
|
3 | 2 | csbeq1d | |
4 | 1 3 | eqtrd | |
5 | csbprc | |
|
6 | csbprc | |
|
7 | 5 6 | eqtr4d | |
8 | 4 7 | pm2.61i | |