MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sbcnestgf Structured version   Visualization version   Unicode version

Theorem sbcnestgf 3796
Description: Nest the composition of two substitutions. (Contributed by Mario Carneiro, 11-Nov-2016.)
Assertion
Ref Expression
sbcnestgf  |-  ( ( A  e.  V  /\  A. y F/ x ph )  ->  ( [. A  /  x ]. [. B  /  y ]. ph  <->  [. [_ A  /  x ]_ B  / 
y ]. ph ) )

Proof of Theorem sbcnestgf
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 dfsbcq 3281 . . . . 5  |-  ( z  =  A  ->  ( [. z  /  x ]. [. B  /  y ]. ph  <->  [. A  /  x ]. [. B  /  y ]. ph ) )
2 csbeq1 3378 . . . . . 6  |-  ( z  =  A  ->  [_ z  /  x ]_ B  = 
[_ A  /  x ]_ B )
32sbceq1d 3284 . . . . 5  |-  ( z  =  A  ->  ( [. [_ z  /  x ]_ B  /  y ]. ph  <->  [. [_ A  /  x ]_ B  /  y ]. ph ) )
41, 3bibi12d 327 . . . 4  |-  ( z  =  A  ->  (
( [. z  /  x ]. [. B  /  y ]. ph  <->  [. [_ z  /  x ]_ B  /  y ]. ph )  <->  ( [. A  /  x ]. [. B  /  y ]. ph  <->  [. [_ A  /  x ]_ B  / 
y ]. ph ) ) )
54imbi2d 322 . . 3  |-  ( 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 3060 . . . . 5  |-  z  e. 
_V
76a1i 11 . . . 4  |-  ( A. y F/ x ph  ->  z  e.  _V )
8 csbeq1a 3384 . . . . . 6  |-  ( x  =  z  ->  B  =  [_ z  /  x ]_ B )
98sbceq1d 3284 . . . . 5  |-  ( x  =  z  ->  ( [. B  /  y ]. ph  <->  [. [_ z  /  x ]_ B  /  y ]. ph ) )
109adantl 472 . . . 4  |-  ( ( A. y F/ x ph  /\  x  =  z )  ->  ( [. B  /  y ]. ph  <->  [. [_ z  /  x ]_ B  / 
y ]. ph ) )
11 nfnf1 1992 . . . . 5  |-  F/ x F/ x ph
1211nfal 2041 . . . 4  |-  F/ x A. y F/ x ph
13 nfa1 1990 . . . . 5  |-  F/ y A. y F/ x ph
14 nfcsb1v 3391 . . . . . 6  |-  F/_ x [_ z  /  x ]_ B
1514a1i 11 . . . . 5  |-  ( A. y F/ x ph  ->  F/_ x [_ z  /  x ]_ B )
16 sp 1948 . . . . 5  |-  ( A. y F/ x ph  ->  F/ x ph )
1713, 15, 16nfsbcd 3300 . . . 4  |-  ( A. y F/ x ph  ->  F/ x [. [_ z  /  x ]_ B  / 
y ]. ph )
187, 10, 12, 17sbciedf 3315 . . 3  |-  ( A. y F/ x ph  ->  (
[. z  /  x ]. [. B  /  y ]. ph  <->  [. [_ z  /  x ]_ B  /  y ]. ph ) )
195, 18vtoclg 3119 . 2  |-  ( A  e.  V  ->  ( A. y F/ x ph  ->  ( [. A  /  x ]. [. B  / 
y ]. ph  <->  [. [_ A  /  x ]_ B  / 
y ]. ph ) ) )
2019imp 435 1  |-  ( ( A  e.  V  /\  A. y F/ x ph )  ->  ( [. A  /  x ]. [. B  /  y ]. ph  <->  [. [_ A  /  x ]_ B  / 
y ]. ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 375   A.wal 1453    = wceq 1455   F/wnf 1678    e. wcel 1898   F/_wnfc 2590   _Vcvv 3057   [.wsbc 3279   [_csb 3375
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-v 3059  df-sbc 3280  df-csb 3376
This theorem is referenced by:  csbnestgf  3797  sbcnestg  3798
  Copyright terms: Public domain W3C validator