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	⊢ ⦋ 𝐴 / 𝑦 ⦌ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ 𝐵

Proof

Step	Hyp	Ref	Expression
1		df-csb	⊢ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = { 𝑧 ∣ [ 𝑦 / 𝑥 ] 𝑧 ∈ 𝐵 }
2	1	abeq2i	⊢ ( 𝑧 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↔ [ 𝑦 / 𝑥 ] 𝑧 ∈ 𝐵 )
3	2	sbcbii	⊢ ( [ 𝐴 / 𝑦 ] 𝑧 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↔ [ 𝐴 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝑧 ∈ 𝐵 )
4		sbcco	⊢ ( [ 𝐴 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝑧 ∈ 𝐵 ↔ [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝐵 )
5	3 4	bitri	⊢ ( [ 𝐴 / 𝑦 ] 𝑧 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↔ [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝐵 )
6	5	abbii	⊢ { 𝑧 ∣ [ 𝐴 / 𝑦 ] 𝑧 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 } = { 𝑧 ∣ [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝐵 }
7		df-csb	⊢ ⦋ 𝐴 / 𝑦 ⦌ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = { 𝑧 ∣ [ 𝐴 / 𝑦 ] 𝑧 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 }
8		df-csb	⊢ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 = { 𝑧 ∣ [ 𝐴 / 𝑥 ] 𝑧 ∈ 𝐵 }
9	6 7 8	3eqtr4i	⊢ ⦋ 𝐴 / 𝑦 ⦌ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ 𝐵