Description: A composition law for class substitution. Version of sbcco with a disjoint variable condition, which requires fewer axioms. (Contributed by NM, 26-Sep-2003) Avoid ax-13 . (Revised by Gino Giotto, 10-Jan-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | sbccow | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbcex | |
|
2 | sbcex | |
|
3 | dfsbcq | |
|
4 | dfsbcq | |
|
5 | sbsbc | |
|
6 | 5 | sbbii | |
7 | sbco2vv | |
|
8 | sbsbc | |
|
9 | 6 7 8 | 3bitr3ri | |
10 | sbsbc | |
|
11 | 9 10 | bitri | |
12 | 3 4 11 | vtoclbg | |
13 | 1 2 12 | pm5.21nii | |