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

Theorem rspcva 3338
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 3336 . 2 (𝐴𝐵 → (∀𝑥𝐵 𝜑𝜓))
32imp 444 1 ((𝐴𝐵 ∧ ∀𝑥𝐵 𝜑) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1523  wcel 2030  wral 2941
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-v 3233
This theorem is referenced by:  rexraleqim  3359  fvn0ssdmfun  6390  fveqdmss  6394  fvcofneq  6407  caofinvl  6966  tfisi  7100  suppssov1  7372  wfr3g  7458  wfrlem17  7476  tfrlem1  7517  boxriin  7992  boxcutc  7993  marypha1lem  8380  marypha1  8381  supmo  8399  infmo  8442  wemaplem2  8493  unwdomg  8530  isinffi  8856  dfac9  8996  sornom  9137  fin23lem11  9177  fin1a2lem13  9272  axdc3lem2  9311  winalim2  9556  grothac  9690  nqereu  9789  nnsub  11097  zextle  11488  xrsupsslem  12175  xrinfmsslem  12176  supxrunb1  12187  supxrunb2  12188  injresinjlem  12628  ssnn0fi  12824  suppssfz  12834  faclbnd4lem4  13123  ishashinf  13285  rexuz3  14132  cau3lem  14138  caubnd2  14141  o1co  14361  climcn1  14366  incexclem  14612  dvdsext  15090  cshwsidrepsw  15847  prdsbasprj  16179  mreintcl  16302  isacs2  16361  acsfiel  16362  initoeu1  16708  initoeu2  16713  termoeu1  16715  isdrs2  16986  lublecllem  17035  joinle  17061  meetle  17075  acsdrsel  17214  isacs4lem  17215  isacs5lem  17216  acsdrscl  17217  acsficl  17218  mgmidmo  17306  gsumval2  17327  mrcmndind  17413  dfgrp3lem  17560  symgfix2  17882  odeq  18015  gexid  18042  mplind  19550  gsummoncoe1  19722  psgndiflemB  19994  m2detleiblem3  20483  m2detleiblem4  20484  cpmatmcllem  20571  mp2pm2mplem4  20662  cayleyhamilton1  20745  cmpsublem  21250  cmpsub  21251  hauscmplem  21257  cmpfii  21260  ptpjcn  21462  isufil2  21759  ufileu  21770  isucn2  22130  cfiluweak  22146  lpbl  22355  lmmbr  23102  caussi  23141  mdeglt  23870  deg1lt  23902  ply1divex  23941  plyco0  23993  dgrco  24076  emcllem7  24773  isppw2  24886  pntleme  25342  pntlemp  25344  tglowdim2ln  25591  uvtxnbgrvtx  26341  rusgrnumwwlks  26941  clwwlkf  27010  eupthseg  27184  upgreupthseg  27187  vdgn1frgrv2  27276  frgrregorufr  27305  extwwlkfablem1OLD  27323  grpoidinvlem3  27488  grpoideu  27491  lnconi  29020  fsumiunle  29703  rngurd  29916  tpr2rico  30086  esumiun  30284  ofcfeqd2  30291  0elsiga  30305  sigaclci  30323  dya2icoseg2  30468  signstfvneq0  30777  derangsn  31278  frr3g  31904  fwddifnp1  32397  poimirlem25  33564  poimirlem26  33565  poimirlem30  33569  poimirlem31  33570  poimirlem32  33571  heicant  33574  mblfinlem2  33577  ftc1anc  33623  fdc  33671  bndss  33715  isdrngo2  33887  divrngidl  33957  maxidlmax  33972  cdleme0nex  35895  dihglblem2N  36900  hgmapvs  37500  ismrcd1  37578  nacsfg  37585  isnacs3  37590  nacsfix  37592  mzpcl1  37609  mzpcl2  37610  mzpcong  37856  dnnumch1  37931  fnwe2lem2  37938  aomclem1  37941  aomclem4  37944  aomclem6  37946  lnr2i  38003  hbtlem5  38015  hbt  38017  pwssfi  39525  eliind  39554  rexanuz3  39589  choicefi  39706  fsneq  39712  rnmptbd2lem  39777  rnmptbdlem  39784  suplesup  39868  xralrple2  39883  infxr  39896  infleinf  39901  xralrple4  39902  xralrple3  39903  xrralrecnnge  39926  supxrunb3  39936  supxrleubrnmpt  39945  unb2ltle  39955  suprleubrnmpt  39962  infxrgelbrnmpt  39996  supminfxr  40007  xrpnf  40029  islpcn  40189  limclner  40201  climd  40222  clim2d  40223  limsupmnflem  40270  limsupre3uzlem  40285  liminflelimsuplem  40325  xlimxrre  40375  xlimmnfvlem1  40376  xlimmnfv  40378  xlimpnfvlem1  40380  xlimpnfv  40382  climxlim2lem  40389  cncfshift  40405  cncfperiod  40410  ioodvbdlimc1lem1  40464  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  fourierdlem103  40744  fourierdlem104  40745  etransclem48  40817  salunicl  40854  saluncl  40855  subsaliuncllem  40893  sge0pnffigt  40931  meadjuni  40992  omessle  41033  caragensplit  41035  omeunile  41040  hoidmvlelem2  41131  hoidmvlelem3  41132  hoidmvle  41135  vonvolmbllem  41195  vonvolmbl  41196  pimdecfgtioc  41246  smfpreimalt  41261  smfpreimaltf  41266  smfpreimale  41284  smfpreimagt  41291  smfpreimage  41311  smfmullem4  41322  smfinflem  41344  iccpartimp  41678  iccpartrn  41691  iccpartiun  41695  icceuelpart  41697  reuccatpfxs1  41759  lidldomn1  42246  ply1mulgsumlem2  42500  lindslinindsimp2lem5  42576  lindslinindsimp2  42577  snlindsntor  42585  nn0sumshdiglemA  42738  nn0sumshdiglemB  42739  nn0sumshdig  42742
  Copyright terms: Public domain W3C validator