Metamath Proof Explorer

Theorem csbnestgfw

Description: Nest the composition of two substitutions. Version of csbnestgf with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 23-Nov-2005) (Revised by Gino Giotto, 26-Jan-2024)

Ref Expression
Assertion csbnestgfw 
|- ( ( 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 sbcnestgfw 
 |-  ( ( 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 )