Description: Composition law for chained substitutions into a class. Version of csbco with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 10-Nov-2005) (Revised by Gino Giotto, 10-Jan-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | csbcow | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-csb | |
|
2 | 1 | abeq2i | |
3 | 2 | sbcbii | |
4 | sbccow | |
|
5 | 3 4 | bitri | |
6 | 5 | abbii | |
7 | df-csb | |
|
8 | df-csb | |
|
9 | 6 7 8 | 3eqtr4i | |