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

Theorem rspcva 3580
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 3578 . 2 (𝐴𝐵 → (∀𝑥𝐵 𝜑𝜓))
32imp 408 1 ((𝐴𝐵 ∧ ∀𝑥𝐵 𝜑) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1542  wcel 2107  wral 3065
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3066
This theorem is referenced by:  rexraleqim  3598  fvn0ssdmfun  7026  fveqdmss  7030  fvcofneq  7044  wfr3g  8254  boxriin  8879  boxcutc  8880  marypha1lem  9370  supmo  9389  infmo  9432  unwdomg  9521  frr3g  9693  isinffi  9929  axdc3lem2  10388  grothac  10767  nqereu  10866  nnsub  12198  zextle  12577  xrsupsslem  13227  xrinfmsslem  13228  supxrunb1  13239  supxrunb2  13240  injresinjlem  13693  ssnn0fi  13891  suppssfz  13900  faclbnd4lem4  14197  ishashinf  14363  rexuz3  15234  cau3lem  15240  caubnd2  15243  o1co  15469  climcn1  15475  incexclem  15722  dvdsext  16204  mreintcl  17476  initoeu1  17898  initoeu2  17903  termoeu1  17905  lublecllem  18250  mgmidmo  18516  gsumval2  18542  dfgrp3lem  18846  symgfix2  19199  odeq  19333  gexid  19364  o2timesd  19942  rglcom4d  19943  gsummoncoe1  21678  m2detleiblem3  21981  m2detleiblem4  21982  cpmatmcllem  22070  mp2pm2mplem4  22161  cayleyhamilton1  22244  cmpsublem  22753  cmpsub  22754  cmpfii  22763  ptpjcn  22965  isufil2  23262  ufileu  23273  lmmbr  24625  caussi  24664  plyco0  25556  dgrco  25639  emcllem7  26354  isppw2  26467  addsid1  27279  uvtxnbgrvtx  28344  rusgrnumwwlks  28922  clwwlkf  28994  vdgn1frgrv2  29243  frgrregorufr  29272  grpoidinvlem3  29451  grpoideu  29454  lnconi  30978  fsumiunle  31728  rngurd  32068  tpr2rico  32496  esumiun  32696  0elsiga  32716  sigaclci  32734  dya2icoseg2  32881  derangsn  33767  sat1el2xp  33976  mulsid1  34414  mulsid2  34415  fwddifnp1  34753  poimirlem25  36106  poimirlem26  36107  poimirlem30  36111  poimirlem31  36112  poimirlem32  36113  heicant  36116  mblfinlem2  36119  ftc1anc  36162  fdc  36207  bndss  36248  isdrngo2  36420  divrngidl  36490  maxidlmax  36505  cdleme0nex  38756  dihglblem2N  39760  hgmapvs  40357  ismrcd1  41024  nacsfg  41031  isnacs3  41036  nacsfix  41038  mzpcl1  41055  mzpcl2  41056  mzpcong  41299  dnnumch1  41374  aomclem1  41384  aomclem6  41389  lnr2i  41446  hbtlem5  41458  hbt  41460  pwssfi  43260  rexanuz3  43313  choicefi  43428  fsneq  43434  suplesup  43580  xralrple2  43595  infxr  43608  infleinf  43613  xralrple4  43614  xralrple3  43615  xrralrecnnge  43632  supxrunb3  43641  supxrleubrnmpt  43648  unb2ltle  43657  suprleubrnmpt  43664  infxrgelbrnmpt  43696  supminfxr  43706  xrpnf  43728  islpcn  43887  limclner  43899  climd  43920  clim2d  43921  limsupmnflem  43968  limsupre3uzlem  43983  liminflelimsuplem  44023  xlimpnfxnegmnf  44062  xlimxrre  44079  xlimmnfvlem1  44080  xlimmnfv  44082  xlimpnfvlem1  44084  xlimpnfv  44086  climxlim2lem  44093  ioodvbdlimc1lem1  44179  ioodvbdlimc1lem2  44180  ioodvbdlimc2lem  44182  fourierdlem103  44457  fourierdlem104  44458  etransclem48  44530  saluncl  44565  subsaliuncllem  44605  sge0pnffigt  44644  omessle  44746  caragensplit  44748  omeunile  44753  hoidmvlelem2  44844  hoidmvlelem3  44845  hoidmvle  44848  vonvolmbllem  44908  vonvolmbl  44909  pimdecfgtioc  44963  smfpreimalt  44979  smfpreimaltf  44984  smfpreimale  45002  smfpreimagt  45010  smfpreimage  45030  smfmullem4  45042  smfinflem  45065  iccpartrn  45629  iccpartiun  45633  icceuelpart  45635  lidldomn1  46226  ply1mulgsumlem2  46475  lindslinindsimp2lem5  46550  lindslinindsimp2  46551  snlindsntor  46559  nn0sumshdiglemA  46712  nn0sumshdiglemB  46713  nn0sumshdig  46716
  Copyright terms: Public domain W3C validator