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

Theorem sbcnestgf 3814
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 3301 . . . . 5  |-  ( z  =  A  ->  ( [. z  /  x ]. [. B  /  y ]. ph  <->  [. A  /  x ]. [. B  /  y ]. ph ) )
2 csbeq1 3398 . . . . . 6  |-  ( z  =  A  ->  [_ z  /  x ]_ B  = 
[_ A  /  x ]_ B )
32sbceq1d 3304 . . . . 5  |-  ( z  =  A  ->  ( [. [_ z  /  x ]_ B  /  y ]. ph  <->  [. [_ A  /  x ]_ B  /  y ]. ph ) )
41, 3bibi12d 322 . . . 4  |-  ( z  =  A  ->  (
( [. z  /  x ]. [. B  /  y ]. ph  <->  [. [_ z  /  x ]_ B  /  y ]. ph )  <->  ( [. A  /  x ]. [. B  /  y ]. ph  <->  [. [_ A  /  x ]_ B  / 
y ]. ph ) ) )
54imbi2d 317 . . 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 3083 . . . . 5  |-  z  e. 
_V
76a1i 11 . . . 4  |-  ( A. y F/ x ph  ->  z  e.  _V )
8 csbeq1a 3404 . . . . . 6  |-  ( x  =  z  ->  B  =  [_ z  /  x ]_ B )
98sbceq1d 3304 . . . . 5  |-  ( x  =  z  ->  ( [. B  /  y ]. ph  <->  [. [_ z  /  x ]_ B  /  y ]. ph ) )
109adantl 467 . . . 4  |-  ( ( A. y F/ x ph  /\  x  =  z )  ->  ( [. B  /  y ]. ph  <->  [. [_ z  /  x ]_ B  / 
y ]. ph ) )
11 nfnf1 1958 . . . . 5  |-  F/ x F/ x ph
1211nfal 2007 . . . 4  |-  F/ x A. y F/ x ph
13 nfa1 1956 . . . . 5  |-  F/ y A. y F/ x ph
14 nfcsb1v 3411 . . . . . 6  |-  F/_ x [_ z  /  x ]_ B
1514a1i 11 . . . . 5  |-  ( A. y F/ x ph  ->  F/_ x [_ z  /  x ]_ B )
16 sp 1914 . . . . 5  |-  ( A. y F/ x ph  ->  F/ x ph )
1713, 15, 16nfsbcd 3320 . . . 4  |-  ( A. y F/ x ph  ->  F/ x [. [_ z  /  x ]_ B  / 
y ]. ph )
187, 10, 12, 17sbciedf 3335 . . 3  |-  ( A. y F/ x ph  ->  (
[. z  /  x ]. [. B  /  y ]. ph  <->  [. [_ z  /  x ]_ B  /  y ]. ph ) )
195, 18vtoclg 3139 . 2  |-  ( A  e.  V  ->  ( A. y F/ x ph  ->  ( [. A  /  x ]. [. B  / 
y ]. ph  <->  [. [_ A  /  x ]_ B  / 
y ]. ph ) ) )
2019imp 430 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 187    /\ wa 370   A.wal 1435    = wceq 1437   F/wnf 1661    e. wcel 1872   F/_wnfc 2566   _Vcvv 3080   [.wsbc 3299   [_csb 3395
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-v 3082  df-sbc 3300  df-csb 3396
This theorem is referenced by:  csbnestgf  3815  sbcnestg  3816
  Copyright terms: Public domain W3C validator