Theorem csbco

Description: Composition law for chained substitutions into a class. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker csbcow when possible. (Contributed by NM, 10-Nov-2005) (New usage is discouraged.)

	Ref	Expression
Assertion	csbco	|- [_ 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		sbcco	|- ( [. 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