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

Theorem rspc 2891
Description: Restricted specialization, using implicit substitution. (Contributed by NM, 19-Apr-2005.) (Revised by Mario Carneiro, 11-Oct-2016.)
Hypotheses
Ref Expression
rspc.1  |-  F/ x ps
rspc.2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
rspc  |-  ( A  e.  B  ->  ( A. x  e.  B  ph 
->  ps ) )
Distinct variable groups:    x, A    x, B
Allowed substitution hints:    ph( x)    ps( x)

Proof of Theorem rspc
StepHypRef Expression
1 df-ral 2561 . 2  |-  ( A. x  e.  B  ph  <->  A. x
( x  e.  B  ->  ph ) )
2 nfcv 2432 . . . 4  |-  F/_ x A
3 nfv 1609 . . . . 5  |-  F/ x  A  e.  B
4 rspc.1 . . . . 5  |-  F/ x ps
53, 4nfim 1781 . . . 4  |-  F/ x
( A  e.  B  ->  ps )
6 eleq1 2356 . . . . 5  |-  ( x  =  A  ->  (
x  e.  B  <->  A  e.  B ) )
7 rspc.2 . . . . 5  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
86, 7imbi12d 311 . . . 4  |-  ( x  =  A  ->  (
( x  e.  B  ->  ph )  <->  ( A  e.  B  ->  ps )
) )
92, 5, 8spcgf 2876 . . 3  |-  ( A  e.  B  ->  ( A. x ( x  e.  B  ->  ph )  -> 
( A  e.  B  ->  ps ) ) )
109pm2.43a 45 . 2  |-  ( A  e.  B  ->  ( A. x ( x  e.  B  ->  ph )  ->  ps ) )
111, 10syl5bi 208 1  |-  ( A  e.  B  ->  ( A. x  e.  B  ph 
->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.wal 1530   F/wnf 1534    = wceq 1632    e. wcel 1696   A.wral 2556
This theorem is referenced by:  rspcv  2893  rspc2  2902  disjxiun  4036  pofun  4346  fmptcof  5708  fliftfuns  5829  qliftfuns  6761  xpf1o  7039  iunfi  7160  iundom2g  8178  lble  9722  rlimcld2  12068  sumeq2ii  12182  summolem3  12203  zsum  12207  fsum  12209  fsumf1o  12212  sumss2  12215  fsumcvg2  12216  fsumadd  12227  isummulc2  12241  fsum2dlem  12249  fsumcom2  12253  fsumshftm  12259  fsum0diag2  12261  fsummulc2  12262  fsum00  12272  fsumabs  12275  fsumrelem  12281  fsumrlim  12285  fsumo1  12286  o1fsum  12287  fsumiun  12295  isumshft  12314  pcmpt  12956  invfuc  13864  dprd2d2  15295  txcnp  17330  ptcnplem  17331  prdsdsf  17947  prdsxmet  17949  fsumcn  18390  ovolfiniun  18876  ovoliunnul  18882  volfiniun  18920  iunmbl  18926  limciun  19260  dvfsumle  19384  dvfsumabs  19386  dvfsumlem1  19389  dvfsumlem3  19391  dvfsumlem4  19392  dvfsumrlim  19394  dvfsumrlim2  19395  dvfsum2  19397  itgsubst  19412  fsumvma  20468  dchrisumlema  20653  dchrisumlem2  20655  dchrisumlem3  20656  chirred  22991  cprodeq2ii  24135  prodmolem3  24156  zprod  24160  fprod  24164  fprodf1o  24172  tfisg  24275  prodeq3ii  25411  fprodadd  25455  fprodneg  25481  fprodsub  25482  ofmpteq  26900  mzpsubst  26929  rabdiophlem2  26986
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-v 2803
  Copyright terms: Public domain W3C validator