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	⊢ ( 𝐴 ∈ 𝑉 → ⦋ 𝐴 / 𝑥 ⦌ ⦋ 𝐵 / 𝑥 ⦌ 𝐶 = ⦋ ⦋ 𝐴 / 𝑥 ⦌ 𝐵 / 𝑥 ⦌ 𝐶 )