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

Proof

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