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

Metamath Proof Explorer

Theorem csbnest1g

Description: Nest the composition of two substitutions. (Contributed by NM, 23-May-2006) (Proof shortened by Mario Carneiro, 11-Nov-2016)

Ref Expression
Assertion csbnest1g ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ⦋ 𝐵 / 𝑥 ⦌ 𝐶 = ⦋ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑥 ⦌ 𝐶 )

Proof

Step Hyp Ref Expression
1 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐶
2 1 ax-gen ⊢ ∀ 𝑦 Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐶
3 csbnestgfw ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑦 Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) → ⦋ 𝐴 / 𝑥 ⦌ ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 = ⦋ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑦 ⦌ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
4 2 3 mpan2 ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 = ⦋ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑦 ⦌ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
5 csbcow ⊢ ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 = ⦋ 𝐵 / 𝑥 ⦌ 𝐶
6 5 csbeq2i ⊢ ⦋ 𝐴 / 𝑥 ⦌ ⦋ 𝐵 / 𝑦 ⦌ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 = ⦋ 𝐴 / 𝑥 ⦌ ⦋ 𝐵 / 𝑥 ⦌ 𝐶
7 csbcow ⊢ ⦋ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑦 ⦌ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 = ⦋ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑥 ⦌ 𝐶
8 4 6 7 3eqtr3g ⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ⦋ 𝐵 / 𝑥 ⦌ 𝐶 = ⦋ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑥 ⦌ 𝐶 )