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

Theorem rspcva 3302
Description: Restricted specialization, using implicit substitution. (Contributed by NM, 13-Sep-2005.)
Hypothesis
Ref Expression
rspcv.1 (𝑥 = 𝐴 → (𝜑𝜓))
Assertion
Ref Expression
rspcva ((𝐴𝐵 ∧ ∀𝑥𝐵 𝜑) → 𝜓)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜓,𝑥
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem rspcva
StepHypRef Expression
1 rspcv.1 . . 3 (𝑥 = 𝐴 → (𝜑𝜓))
21rspcv 3300 . 2 (𝐴𝐵 → (∀𝑥𝐵 𝜑𝜓))
32imp 445 1 ((𝐴𝐵 ∧ ∀𝑥𝐵 𝜑) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1481  wcel 1988  wral 2909
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-v 3197
This theorem is referenced by:  rexraleqim  3323  fvn0ssdmfun  6336  fveqdmss  6340  fvcofneq  6353  caofinvl  6909  tfisi  7043  suppssov1  7312  wfr3g  7398  wfrlem17  7416  tfrlem1  7457  boxriin  7935  boxcutc  7936  marypha1lem  8324  marypha1  8325  supmo  8343  infmo  8386  wemaplem2  8437  unwdomg  8474  isinffi  8803  dfac9  8943  sornom  9084  fin23lem11  9124  fin1a2lem13  9219  axdc3lem2  9258  winalim2  9503  grothac  9637  nqereu  9736  nnsub  11044  zextle  11435  xrsupsslem  12122  xrinfmsslem  12123  supxrunb1  12134  supxrunb2  12135  injresinjlem  12571  ssnn0fi  12767  suppssfz  12777  faclbnd4lem4  13066  ishashinf  13230  rexuz3  14069  cau3lem  14075  caubnd2  14078  o1co  14298  climcn1  14303  incexclem  14549  dvdsext  15024  cshwsidrepsw  15781  prdsbasprj  16113  mreintcl  16236  isacs2  16295  acsfiel  16296  initoeu1  16642  initoeu2  16647  termoeu1  16649  isdrs2  16920  lublecllem  16969  joinle  16995  meetle  17009  acsdrsel  17148  isacs4lem  17149  isacs5lem  17150  acsdrscl  17151  acsficl  17152  mgmidmo  17240  gsumval2  17261  mrcmndind  17347  dfgrp3lem  17494  symgfix2  17817  odeq  17950  gexid  17977  mplind  19483  gsummoncoe1  19655  psgndiflemB  19927  m2detleiblem3  20416  m2detleiblem4  20417  cpmatmcllem  20504  mp2pm2mplem4  20595  cayleyhamilton1  20678  cmpsublem  21183  cmpsub  21184  hauscmplem  21190  cmpfii  21193  ptpjcn  21395  isufil2  21693  ufileu  21704  isucn2  22064  cfiluweak  22080  lpbl  22289  lmmbr  23037  caussi  23076  mdeglt  23806  deg1lt  23838  ply1divex  23877  plyco0  23929  dgrco  24012  emcllem7  24709  isppw2  24822  pntleme  25278  pntlemp  25280  tglowdim2ln  25527  uvtxanbgrvtx  26274  rusgrnumwwlks  26850  clwwlksf  26895  eupthseg  27046  upgreupthseg  27049  vdgn1frgrv2  27140  frgrregorufr  27163  extwwlkfablem1  27182  grpoidinvlem3  27330  grpoideu  27333  lnconi  28862  fsumiunle  29549  rngurd  29762  tpr2rico  29932  esumiun  30130  ofcfeqd2  30137  0elsiga  30151  sigaclci  30169  dya2icoseg2  30314  signstfvneq0  30623  derangsn  31126  frr3g  31753  fwddifnp1  32247  poimirlem25  33405  poimirlem26  33406  poimirlem30  33410  poimirlem31  33411  poimirlem32  33412  heicant  33415  mblfinlem2  33418  ftc1anc  33464  fdc  33512  bndss  33556  isdrngo2  33728  divrngidl  33798  maxidlmax  33813  cdleme0nex  35396  dihglblem2N  36402  hgmapvs  37002  ismrcd1  37080  nacsfg  37087  isnacs3  37092  nacsfix  37094  mzpcl1  37111  mzpcl2  37112  mzpcong  37358  dnnumch1  37433  fnwe2lem2  37440  aomclem1  37443  aomclem4  37446  aomclem6  37448  lnr2i  37505  hbtlem5  37517  hbt  37519  pwssfi  39031  eliind  39060  rexanuz3  39095  choicefi  39208  fsneq  39214  rnmptbd2lem  39279  rnmptbdlem  39286  suplesup  39368  xralrple2  39383  infxr  39396  infleinf  39401  xralrple4  39402  xralrple3  39403  xrralrecnnge  39426  supxrunb3  39436  supxrleubrnmpt  39445  unb2ltle  39455  suprleubrnmpt  39462  infxrgelbrnmpt  39496  supminfxr  39507  islpcn  39671  limclner  39683  climd  39704  clim2d  39705  limsupmnflem  39752  limsupre3uzlem  39767  liminflelimsuplem  39801  cncfshift  39850  cncfperiod  39855  ioodvbdlimc1lem1  39909  ioodvbdlimc1lem2  39910  ioodvbdlimc2lem  39912  fourierdlem103  40189  fourierdlem104  40190  etransclem48  40262  salunicl  40299  saluncl  40300  subsaliuncllem  40338  sge0pnffigt  40376  meadjuni  40437  omessle  40475  caragensplit  40477  omeunile  40482  hoidmvlelem2  40573  hoidmvlelem3  40574  hoidmvle  40577  vonvolmbllem  40637  vonvolmbl  40638  pimdecfgtioc  40688  smfpreimalt  40703  smfpreimaltf  40708  smfpreimale  40726  smfpreimagt  40733  smfpreimage  40753  smfmullem4  40764  smfinflem  40786  iccpartimp  41117  iccpartrn  41130  iccpartiun  41134  icceuelpart  41136  reuccatpfxs1  41199  lidldomn1  41686  ply1mulgsumlem2  41940  lindslinindsimp2lem5  42016  lindslinindsimp2  42017  snlindsntor  42025  nn0sumshdiglemA  42178  nn0sumshdiglemB  42179  nn0sumshdig  42182
  Copyright terms: Public domain W3C validator