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 ⊢ A ∈ V → ⦋ A / x⦌ ⦋ B / x⦌ C = ⦋ ⦋ A / x⦌ B / x⦌ C

Proof

Step Hyp Ref Expression
1 nfcsb1v ⊢ Ⅎ _ x ⦋ y / x⦌ C
2 1 ax-gen ⊢ ∀ y Ⅎ _ x ⦋ y / x⦌ C
3 csbnestgfw ⊢ A ∈ V ∧ ∀ y Ⅎ _ x ⦋ y / x⦌ C → ⦋ A / x⦌ ⦋ B / y⦌ ⦋ y / x⦌ C = ⦋ ⦋ A / x⦌ B / y⦌ ⦋ y / x⦌ C
4 2 3 mpan2 ⊢ A ∈ V → ⦋ A / x⦌ ⦋ B / y⦌ ⦋ y / x⦌ C = ⦋ ⦋ A / x⦌ B / y⦌ ⦋ y / x⦌ C
5 csbcow ⊢ ⦋ B / y⦌ ⦋ y / x⦌ C = ⦋ B / x⦌ C
6 5 csbeq2i ⊢ ⦋ A / x⦌ ⦋ B / y⦌ ⦋ y / x⦌ C = ⦋ A / x⦌ ⦋ B / x⦌ C
7 csbcow ⊢ ⦋ ⦋ A / x⦌ B / y⦌ ⦋ y / x⦌ C = ⦋ ⦋ A / x⦌ B / x⦌ C
8 4 6 7 3eqtr3g ⊢ A ∈ V → ⦋ A / x⦌ ⦋ B / x⦌ C = ⦋ ⦋ A / x⦌ B / x⦌ C