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 / y ]_ [_ y / x ]_ B = [_ A / x ]_ B

Proof

Step	Hyp	Ref	Expression
1		df-csb	|- [_ y / x ]_ B = { z | [. y / x ]. z e. B }
2	1	abeq2i	|- ( z e. [_ y / x ]_ B <-> [. y / x ]. z e. B )
3	2	sbcbii	|- ( [. A / y ]. z e. [_ y / x ]_ B <-> [. A / y ]. [. y / x ]. z e. B )
4		sbccow	|- ( [. A / y ]. [. y / x ]. z e. B <-> [. A / x ]. z e. B )
5	3 4	bitri	|- ( [. A / y ]. z e. [_ y / x ]_ B <-> [. A / x ]. z e. B )
6	5	abbii	|- { z | [. A / y ]. z e. [_ y / x ]_ B } = { z | [. A / x ]. z e. B }
7		df-csb	|- [_ A / y ]_ [_ y / x ]_ B = { z | [. A / y ]. z e. [_ y / x ]_ B }
8		df-csb	|- [_ A / x ]_ B = { z | [. A / x ]. z e. B }
9	6 7 8	3eqtr4i	|- [_ A / y ]_ [_ y / x ]_ B = [_ A / x ]_ B