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 e. V -> [_ A / x ]_ [_ B / x ]_ C = [_ [_ A / x ]_ B / x ]_ C )

Proof

Step Hyp Ref Expression
1 nfcsb1v 
 |-  F/_ x [_ y / x ]_ C
2 1 ax-gen 
 |-  A. y F/_ x [_ y / x ]_ C
3 csbnestgfw 
 |-  ( ( A e. V /\ A. y F/_ x [_ y / x ]_ C ) -> [_ A / x ]_ [_ B / y ]_ [_ y / x ]_ C = [_ [_ A / x ]_ B / y ]_ [_ y / x ]_ C )
4 2 3 mpan2 
 |-  ( A e. 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 e. V -> [_ A / x ]_ [_ B / x ]_ C = [_ [_ A / x ]_ B / x ]_ C )