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

Theorem sbcimg 3228
Description: Distribution of class substitution over implication. (Contributed by NM, 16-Jan-2004.)
Assertion
Ref Expression
sbcimg  |-  ( A  e.  V  ->  ( [. A  /  x ]. ( ph  ->  ps ) 
<->  ( [. A  /  x ]. ph  ->  [. A  /  x ]. ps )
) )

Proof of Theorem sbcimg
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 dfsbcq2 3189 . 2  |-  ( y  =  A  ->  ( [ y  /  x ] ( ph  ->  ps )  <->  [. A  /  x ]. ( ph  ->  ps ) ) )
2 dfsbcq2 3189 . . 3  |-  ( y  =  A  ->  ( [ y  /  x ] ph  <->  [. A  /  x ]. ph ) )
3 dfsbcq2 3189 . . 3  |-  ( y  =  A  ->  ( [ y  /  x ] ps  <->  [. A  /  x ]. ps ) )
42, 3imbi12d 320 . 2  |-  ( y  =  A  ->  (
( [ y  /  x ] ph  ->  [ y  /  x ] ps ) 
<->  ( [. A  /  x ]. ph  ->  [. A  /  x ]. ps )
) )
5 sbim 2087 . 2  |-  ( [ y  /  x ]
( ph  ->  ps )  <->  ( [ y  /  x ] ph  ->  [ y  /  x ] ps )
)
61, 4, 5vtoclbg 3031 1  |-  ( A  e.  V  ->  ( [. A  /  x ]. ( ph  ->  ps ) 
<->  ( [. A  /  x ]. ph  ->  [. A  /  x ]. ps )
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1369   [wsb 1700    e. wcel 1756   [.wsbc 3186
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-v 2974  df-sbc 3187
This theorem is referenced by:  sbcim1  3235  sbceqal  3242  sbcimdvOLD  3256  sbc19.21g  3259  sbcssg  3790  iota4an  5400  sbcfung  5441  riotass2  6079  tfinds2  6474  sbcimi  28915  telescgsum  30811  sbcim2g  31245  sbcssOLD  31249  onfrALTlem5  31250  sbcim2gVD  31611  sbcssgVD  31619  onfrALTlem5VD  31621  bnj538  31732  bnj110  31851  bnj92  31855  bnj539  31884  bnj540  31885  cdlemkid3N  34577  cdlemkid4  34578  cdlemk35s  34581  cdlemk39s  34583  cdlemk42  34585
  Copyright terms: Public domain W3C validator