Metamath Proof Explorer

Theorem csbnestgf

Description: Nest the composition of two substitutions. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker csbnestgfw when possible. (Contributed by NM, 23-Nov-2005) (Proof shortened by Mario Carneiro, 10-Nov-2016) (New usage is discouraged.)

Ref Expression
Assertion csbnestgf 
|- ( ( A e. V /\ A. y F/_ x C ) -> [_ A / x ]_ [_ B / y ]_ C = [_ [_ A / x ]_ B / y ]_ C )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( A e. V -> A e. _V )
2 df-csb 
 |-  [_ B / y ]_ C = { z | [. B / y ]. z e. C }
3 2 abeq2i 
 |-  ( z e. [_ B / y ]_ C <-> [. B / y ]. z e. C )
4 3 sbcbii 
 |-  ( [. A / x ]. z e. [_ B / y ]_ C <-> [. A / x ]. [. B / y ]. z e. C )
5 nfcr 
 |-  ( F/_ x C -> F/ x z e. C )
6 5 alimi 
 |-  ( A. y F/_ x C -> A. y F/ x z e. C )
7 sbcnestgf 
 |-  ( ( A e. _V /\ A. y F/ x z e. C ) -> ( [. A / x ]. [. B / y ]. z e. C <-> [. [_ A / x ]_ B / y ]. z e. C ) )
8 6 7 sylan2 
 |-  ( ( A e. _V /\ A. y F/_ x C ) -> ( [. A / x ]. [. B / y ]. z e. C <-> [. [_ A / x ]_ B / y ]. z e. C ) )
9 4 8 bitrid 
 |-  ( ( A e. _V /\ A. y F/_ x C ) -> ( [. A / x ]. z e. [_ B / y ]_ C <-> [. [_ A / x ]_ B / y ]. z e. C ) )
10 9 abbidv 
 |-  ( ( A e. _V /\ A. y F/_ x C ) -> { z | [. A / x ]. z e. [_ B / y ]_ C } = { z | [. [_ A / x ]_ B / y ]. z e. C } )
11 1 10 sylan 
 |-  ( ( A e. V /\ A. y F/_ x C ) -> { z | [. A / x ]. z e. [_ B / y ]_ C } = { z | [. [_ A / x ]_ B / y ]. z e. C } )
12 df-csb 
 |-  [_ A / x ]_ [_ B / y ]_ C = { z | [. A / x ]. z e. [_ B / y ]_ C }
13 df-csb 
 |-  [_ [_ A / x ]_ B / y ]_ C = { z | [. [_ A / x ]_ B / y ]. z e. C }
14 11 12 13 3eqtr4g 
 |-  ( ( A e. V /\ A. y F/_ x C ) -> [_ A / x ]_ [_ B / y ]_ C = [_ [_ A / x ]_ B / y ]_ C )