Metamath Proof Explorer

Theorem sbcnestgfw

Description: Nest the composition of two substitutions. Version of sbcnestgf with a disjoint variable condition, which does not require ax-13 . (Contributed by Mario Carneiro, 11-Nov-2016) (Revised by Gino Giotto, 26-Jan-2024)

Ref Expression
Assertion sbcnestgfw 
|- ( ( A e. V /\ A. y F/ x ph ) -> ( [. A / x ]. [. B / y ]. ph <-> [. [_ A / x ]_ B / y ]. ph ) )

Proof

Step Hyp Ref Expression
1 dfsbcq 
 |-  ( z = A -> ( [. z / x ]. [. B / y ]. ph <-> [. A / x ]. [. B / y ]. ph ) )
2 csbeq1 
 |-  ( z = A -> [_ z / x ]_ B = [_ A / x ]_ B )
3 2 sbceq1d 
 |-  ( z = A -> ( [. [_ z / x ]_ B / y ]. ph <-> [. [_ A / x ]_ B / y ]. ph ) )
4 1 3 bibi12d 
 |-  ( z = A -> ( ( [. z / x ]. [. B / y ]. ph <-> [. [_ z / x ]_ B / y ]. ph ) <-> ( [. A / x ]. [. B / y ]. ph <-> [. [_ A / x ]_ B / y ]. ph ) ) )
5 4 imbi2d 
 |-  ( z = A -> ( ( A. y F/ x ph -> ( [. z / x ]. [. B / y ]. ph <-> [. [_ z / x ]_ B / y ]. ph ) ) <-> ( A. y F/ x ph -> ( [. A / x ]. [. B / y ]. ph <-> [. [_ A / x ]_ B / y ]. ph ) ) ) )
6 vex 
 |-  z e. _V
7 6 a1i 
 |-  ( A. y F/ x ph -> z e. _V )
8 csbeq1a 
 |-  ( x = z -> B = [_ z / x ]_ B )
9 8 sbceq1d 
 |-  ( x = z -> ( [. B / y ]. ph <-> [. [_ z / x ]_ B / y ]. ph ) )
10 9 adantl 
 |-  ( ( A. y F/ x ph /\ x = z ) -> ( [. B / y ]. ph <-> [. [_ z / x ]_ B / y ]. ph ) )
11 nfnf1 
 |-  F/ x F/ x ph
12 11 nfal 
 |-  F/ x A. y F/ x ph
13 nfa1 
 |-  F/ y A. y F/ x ph
14 nfcsb1v 
 |-  F/_ x [_ z / x ]_ B
15 14 a1i 
 |-  ( A. y F/ x ph -> F/_ x [_ z / x ]_ B )
16 sp 
 |-  ( A. y F/ x ph -> F/ x ph )
17 13 15 16 nfsbcdw 
 |-  ( A. y F/ x ph -> F/ x [. [_ z / x ]_ B / y ]. ph )
18 7 10 12 17 sbciedf 
 |-  ( A. y F/ x ph -> ( [. z / x ]. [. B / y ]. ph <-> [. [_ z / x ]_ B / y ]. ph ) )
19 5 18 vtoclg 
 |-  ( A e. V -> ( A. y F/ x ph -> ( [. A / x ]. [. B / y ]. ph <-> [. [_ A / x ]_ B / y ]. ph ) ) )
20 19 imp 
 |-  ( ( A e. V /\ A. y F/ x ph ) -> ( [. A / x ]. [. B / y ]. ph <-> [. [_ A / x ]_ B / y ]. ph ) )