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

Theorem rspcva 3279
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 3277 . 2 (𝐴𝐵 → (∀𝑥𝐵 𝜑𝜓))
32imp 443 1 ((𝐴𝐵 ∧ ∀𝑥𝐵 𝜑) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382   = wceq 1474  wcel 1976  wral 2895
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-v 3174
This theorem is referenced by:  rexraleqim  3298  fvn0ssdmfun  6243  fveqdmss  6247  fvcofneq  6260  caofinvl  6799  tfisi  6927  suppssov1  7191  wfr3g  7277  wfrlem17  7295  tfrlem1  7336  boxriin  7813  boxcutc  7814  marypha1lem  8199  marypha1  8200  supmo  8218  infmo  8261  wemaplem2  8312  unwdomg  8349  isinffi  8678  dfac9  8818  sornom  8959  fin23lem11  8999  fin1a2lem13  9094  axdc3lem2  9133  winalim2  9374  grothac  9508  nqereu  9607  nnsub  10906  zextle  11282  xrsupsslem  11965  xrinfmsslem  11966  supxrunb1  11977  supxrunb2  11978  injresinjlem  12405  ssnn0fi  12601  suppssfz  12611  faclbnd4lem4  12900  ishashinf  13056  rexuz3  13882  cau3lem  13888  caubnd2  13891  o1co  14111  climcn1  14116  incexclem  14353  dvdsext  14827  cshwsidrepsw  15584  prdsbasprj  15901  mreintcl  16024  isacs2  16083  acsfiel  16084  initoeu1  16430  initoeu2  16435  termoeu1  16437  isdrs2  16708  lublecllem  16757  joinle  16783  meetle  16797  acsdrsel  16936  isacs4lem  16937  isacs5lem  16938  acsdrscl  16939  acsficl  16940  mgmidmo  17028  gsumval2  17049  mrcmndind  17135  dfgrp3lem  17282  symgfix2  17605  odeq  17738  gexid  17765  mplind  19269  gsummoncoe1  19441  psgndiflemB  19710  mdetunilem1  20179  m2detleiblem3  20196  m2detleiblem4  20197  cpmatmcllem  20284  mp2pm2mplem4  20375  cayleyhamilton1  20458  cmpsublem  20954  cmpsub  20955  hauscmplem  20961  cmpfii  20964  ptpjcn  21166  isufil2  21464  ufileu  21475  isucn2  21835  cfiluweak  21851  cuspcvg  21857  lpbl  22059  lmmbr  22782  caussi  22821  mdeglt  23546  deg1lt  23578  ply1divex  23617  plyco0  23669  dgrco  23752  emcllem7  24445  isppw2  24558  pntleme  25014  pntlemp  25016  tglowdim2ln  25264  nbcusgra  25758  uvtxnbgra  25787  wlkdvspthlem  25903  clwwlkf  26088  rusgranumwlks  26249  frgraunss  26288  vdn0frgrav2  26316  vdgn0frgrav2  26317  vdn1frgrav2  26318  vdgn1frgrav2  26319  frgrancvvdeqlem4  26326  frgraregorufr  26346  extwwlkfablem1  26367  grpoidinvlem3  26510  grpoideu  26513  lnconi  28082  rngurd  28925  tpr2rico  29092  esumiun  29289  ofcfeqd2  29296  0elsiga  29310  sigaclci  29328  dya2icoseg2  29473  signstfvneq0  29781  derangsn  30212  frr3g  30829  fwddifnp1  31248  poimirlem25  32400  poimirlem26  32401  poimirlem30  32405  poimirlem31  32406  poimirlem32  32407  heicant  32410  mblfinlem2  32413  ftc1anc  32459  fdc  32507  bndss  32551  isdrngo2  32723  divrngidl  32793  maxidlmax  32808  cdleme0nex  34391  dihglblem2N  35397  hgmapvs  35997  ismrcd1  36075  nacsfg  36082  isnacs3  36087  nacsfix  36089  mzpcl1  36106  mzpcl2  36107  mzpcong  36353  dnnumch1  36428  fnwe2lem2  36435  aomclem1  36438  aomclem4  36441  aomclem6  36443  lnr2i  36501  hbtlem5  36513  hbt  36515  pwssfi  38032  eliind  38062  rexanuz3  38099  choicefi  38183  fsneq  38189  suplesup  38293  xralrple2  38308  infxr  38321  infleinf  38326  xralrple4  38327  xralrple3  38328  xrralrecnnge  38351  islpcn  38503  limclner  38515  climd  38536  clim2d  38537  cncfshift  38556  cncfperiod  38561  ioodvbdlimc1lem1  38618  ioodvbdlimc1lem2  38619  ioodvbdlimc2lem  38621  fourierdlem103  38899  fourierdlem104  38900  etransclem48  38972  salunicl  39009  saluncl  39010  saldifcl  39012  subsaliuncllem  39048  sge0pnffigt  39086  meadjuni  39147  omessle  39185  caragensplit  39187  omeunile  39192  hoidmvlelem2  39283  hoidmvlelem3  39284  hoidmvle  39287  vonvolmbllem  39347  vonvolmbl  39348  pimdecfgtioc  39399  smfpreimalt  39414  smfpreimaltf  39420  smfpreimale  39438  smfpreimagt  39445  smfpreimage  39465  smfmullem4  39476  iccpartimp  39753  iccpartrn  39766  iccpartiun  39770  icceuelpart  39772  reuccatpfxs1  40095  n0snor2el  40116  uvtxanbgrvtx  40614  rusgrnumwwlks  41172  clwwlksf  41217  eupthseg  41369  upgreupthseg  41372  vdgn1frgrv2  41461  frgrncvvdeqlem4  41467  frgrregorufr  41485  av-extwwlkfablem1  41503  lidldomn1  41706  ply1mulgsumlem2  41964  lindslinindsimp2lem5  42040  lindslinindsimp2  42041  snlindsntor  42049  nn0sumshdiglemA  42206  nn0sumshdiglemB  42207  nn0sumshdig  42210
  Copyright terms: Public domain W3C validator