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 ) )