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

Theorem rspcva 3455
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 3453 . 2 (𝐴𝐵 → (∀𝑥𝐵 𝜑𝜓))
32imp 443 1 ((𝐴𝐵 ∧ ∀𝑥𝐵 𝜑) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1629  wcel 2143  wral 3059
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1868  ax-4 1883  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2152  ax-10 2172  ax-11 2188  ax-12 2201  ax-13 2406  ax-ext 2749
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1632  df-ex 1851  df-nf 1856  df-sb 2048  df-clab 2756  df-cleq 2762  df-clel 2765  df-nfc 2900  df-ral 3064  df-v 3350
This theorem is referenced by:  rexraleqim  3475  fvn0ssdmfun  6492  fveqdmss  6496  fvcofneq  6509  wfr3g  7563  boxriin  8102  boxcutc  8103  marypha1lem  8493  supmo  8512  infmo  8555  unwdomg  8643  isinffi  9016  axdc3lem2  9473  grothac  9852  nqereu  9951  nnsub  11259  zextle  11650  xrsupsslem  12341  xrinfmsslem  12342  supxrunb1  12353  supxrunb2  12354  injresinjlem  12795  ssnn0fi  12991  suppssfz  13001  faclbnd4lem4  13290  ishashinf  13452  rexuz3  14299  cau3lem  14305  caubnd2  14308  o1co  14528  climcn1  14533  incexclem  14779  dvdsext  15257  mreintcl  16469  initoeu1  16874  initoeu2  16879  termoeu1  16881  lublecllem  17202  mgmidmo  17473  gsumval2  17494  dfgrp3lem  17727  symgfix2  18049  odeq  18182  gexid  18209  gsummoncoe1  19895  m2detleiblem3  20659  m2detleiblem4  20660  cpmatmcllem  20749  mp2pm2mplem4  20840  cayleyhamilton1  20923  cmpsublem  21429  cmpsub  21430  cmpfii  21439  ptpjcn  21641  isufil2  21938  ufileu  21949  lmmbr  23281  caussi  23320  plyco0  24174  dgrco  24257  emcllem7  24955  isppw2  25068  uvtxnbgrvtx  26526  rusgrnumwwlks  27127  clwwlkf  27207  eupthseg  27390  upgreupthseg  27393  vdgn1frgrv2  27482  frgrregorufr  27511  extwwlkfablem1OLD  27529  grpoidinvlem3  27701  grpoideu  27704  lnconi  29233  fsumiunle  29916  rngurd  30129  tpr2rico  30299  esumiun  30497  ofcfeqd2  30504  0elsiga  30518  sigaclci  30536  dya2icoseg2  30681  signstfvneq0  30990  derangsn  31491  frr3g  32117  fwddifnp1  32610  poimirlem25  33767  poimirlem26  33768  poimirlem30  33772  poimirlem31  33773  poimirlem32  33774  heicant  33777  mblfinlem2  33780  ftc1anc  33825  fdc  33873  bndss  33917  isdrngo2  34089  divrngidl  34159  maxidlmax  34174  cdleme0nex  36099  dihglblem2N  37104  hgmapvs  37701  ismrcd1  37787  nacsfg  37794  isnacs3  37799  nacsfix  37801  mzpcl1  37818  mzpcl2  37819  mzpcong  38065  dnnumch1  38140  fnwe2lem2  38147  aomclem1  38150  aomclem4  38153  aomclem6  38155  lnr2i  38212  hbtlem5  38224  hbt  38226  pwssfi  39733  eliind  39762  rexanuz3  39797  choicefi  39911  fsneq  39917  rnmptbd2lem  39982  rnmptbdlem  39989  suplesup  40072  xralrple2  40087  infxr  40100  infleinf  40105  xralrple4  40106  xralrple3  40107  xrralrecnnge  40130  supxrunb3  40140  supxrleubrnmpt  40149  unb2ltle  40159  suprleubrnmpt  40166  infxrgelbrnmpt  40200  supminfxr  40211  xrpnf  40233  islpcn  40390  limclner  40402  climd  40423  clim2d  40424  limsupmnflem  40471  limsupre3uzlem  40486  liminflelimsuplem  40526  xlimxrre  40576  xlimmnfvlem1  40577  xlimmnfv  40579  xlimpnfvlem1  40581  xlimpnfv  40583  climxlim2lem  40590  cncfshift  40606  cncfperiod  40611  ioodvbdlimc1lem1  40665  ioodvbdlimc1lem2  40666  ioodvbdlimc2lem  40668  fourierdlem103  40944  fourierdlem104  40945  etransclem48  41017  salunicl  41054  saluncl  41055  subsaliuncllem  41093  sge0pnffigt  41131  meadjuni  41192  omessle  41233  caragensplit  41235  omeunile  41240  hoidmvlelem2  41331  hoidmvlelem3  41332  hoidmvle  41335  vonvolmbllem  41395  vonvolmbl  41396  pimdecfgtioc  41446  smfpreimalt  41461  smfpreimaltf  41466  smfpreimale  41484  smfpreimagt  41491  smfpreimage  41511  smfmullem4  41522  smfinflem  41544  iccpartimp  41878  iccpartrn  41891  iccpartiun  41895  icceuelpart  41897  reuccatpfxs1  41959  lidldomn1  42446  ply1mulgsumlem2  42700  lindslinindsimp2lem5  42776  lindslinindsimp2  42777  snlindsntor  42785  nn0sumshdiglemA  42938  nn0sumshdiglemB  42939  nn0sumshdig  42942
  Copyright terms: Public domain W3C validator