Metamath Proof Explorer


Theorem csbcow

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 A/yy/xB=A/xB

Proof

Step Hyp Ref Expression
1 df-csb y/xB=z|[˙y/x]˙zB
2 1 abeq2i zy/xB[˙y/x]˙zB
3 2 sbcbii [˙A/y]˙zy/xB[˙A/y]˙[˙y/x]˙zB
4 sbccow [˙A/y]˙[˙y/x]˙zB[˙A/x]˙zB
5 3 4 bitri [˙A/y]˙zy/xB[˙A/x]˙zB
6 5 abbii z|[˙A/y]˙zy/xB=z|[˙A/x]˙zB
7 df-csb A/yy/xB=z|[˙A/y]˙zy/xB
8 df-csb A/xB=z|[˙A/x]˙zB
9 6 7 8 3eqtr4i A/yy/xB=A/xB