This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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) Avoid ax-13 . (Revised by GG, 10-Jan-2024)

Ref Expression
Assertion csbcow ⦋ 𝐴 / 𝑦 ⦌ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = ⦋ 𝐴 / 𝑥 ⦌ 𝐵

Proof

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