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)