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

Theorem sbcco3g 3818
Description: Composition of two substitutions. (Contributed by NM, 27-Nov-2005.) (Revised by Mario Carneiro, 11-Nov-2016.)
Hypothesis
Ref Expression
sbcco3g.1  |-  ( x  =  A  ->  B  =  C )
Assertion
Ref Expression
sbcco3g  |-  ( A  e.  V  ->  ( [. A  /  x ]. [. B  /  y ]. ph  <->  [. C  /  y ]. ph ) )
Distinct variable groups:    x, A    ph, x    x, C
Allowed substitution hints:    ph( y)    A( y)    B( x, y)    C( y)    V( x, y)

Proof of Theorem sbcco3g
StepHypRef Expression
1 sbcnestg 3816 . 2  |-  ( A  e.  V  ->  ( [. A  /  x ]. [. B  /  y ]. ph  <->  [. [_ A  /  x ]_ B  /  y ]. ph ) )
2 elex 3089 . . 3  |-  ( A  e.  V  ->  A  e.  _V )
3 nfcvd 2581 . . . 4  |-  ( A  e.  _V  ->  F/_ x C )
4 sbcco3g.1 . . . 4  |-  ( x  =  A  ->  B  =  C )
53, 4csbiegf 3419 . . 3  |-  ( A  e.  _V  ->  [_ A  /  x ]_ B  =  C )
6 dfsbcq 3301 . . 3  |-  ( [_ A  /  x ]_ B  =  C  ->  ( [. [_ A  /  x ]_ B  /  y ]. ph  <->  [. C  / 
y ]. ph ) )
72, 5, 63syl 18 . 2  |-  ( A  e.  V  ->  ( [. [_ A  /  x ]_ B  /  y ]. ph  <->  [. C  /  y ]. ph ) )
81, 7bitrd 256 1  |-  ( A  e.  V  ->  ( [. A  /  x ]. [. B  /  y ]. ph  <->  [. C  /  y ]. ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    = wceq 1437    e. wcel 1872   _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:  fzshftral  11890  2rexfrabdioph  35609  3rexfrabdioph  35610  4rexfrabdioph  35611  6rexfrabdioph  35612  7rexfrabdioph  35613
  Copyright terms: Public domain W3C validator