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

Theorem rspcva 3618
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 3615 . 2 (𝐴𝐵 → (∀𝑥𝐵 𝜑𝜓))
32imp 407 1 ((𝐴𝐵 ∧ ∀𝑥𝐵 𝜑) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1528  wcel 2105  wral 3135
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2811  df-clel 2890  df-ral 3140
This theorem is referenced by:  rexraleqim  3637  fvn0ssdmfun  6834  fveqdmss  6838  fvcofneq  6851  wfr3g  7942  boxriin  8492  boxcutc  8493  marypha1lem  8885  supmo  8904  infmo  8947  unwdomg  9036  isinffi  9409  axdc3lem2  9861  grothac  10240  nqereu  10339  nnsub  11669  zextle  12043  xrsupsslem  12688  xrinfmsslem  12689  supxrunb1  12700  supxrunb2  12701  injresinjlem  13145  ssnn0fi  13341  suppssfz  13350  faclbnd4lem4  13644  ishashinf  13809  rexuz3  14696  cau3lem  14702  caubnd2  14705  o1co  14931  climcn1  14936  incexclem  15179  dvdsext  15659  mreintcl  16854  initoeu1  17259  initoeu2  17264  termoeu1  17266  lublecllem  17586  mgmidmo  17858  gsumval2  17884  dfgrp3lem  18135  symgfix2  18473  odeq  18607  gexid  18635  gsummoncoe1  20400  m2detleiblem3  21166  m2detleiblem4  21167  cpmatmcllem  21254  mp2pm2mplem4  21345  cayleyhamilton1  21428  cmpsublem  21935  cmpsub  21936  cmpfii  21945  ptpjcn  22147  isufil2  22444  ufileu  22455  lmmbr  23788  caussi  23827  plyco0  24709  dgrco  24792  emcllem7  25506  isppw2  25619  uvtxnbgrvtx  27102  rusgrnumwwlks  27680  clwwlkf  27753  vdgn1frgrv2  28002  frgrregorufr  28031  grpoidinvlem3  28210  grpoideu  28213  lnconi  29737  fsumiunle  30472  rngurd  30784  tpr2rico  31054  esumiun  31252  0elsiga  31272  sigaclci  31290  dya2icoseg2  31435  derangsn  32314  sat1el2xp  32523  frr3g  33018  fwddifnp1  33523  poimirlem25  34798  poimirlem26  34799  poimirlem30  34803  poimirlem31  34804  poimirlem32  34805  heicant  34808  mblfinlem2  34811  ftc1anc  34856  fdc  34901  bndss  34945  isdrngo2  35117  divrngidl  35187  maxidlmax  35202  cdleme0nex  37306  dihglblem2N  38310  hgmapvs  38907  ismrcd1  39173  nacsfg  39180  isnacs3  39185  nacsfix  39187  mzpcl1  39204  mzpcl2  39205  mzpcong  39447  dnnumch1  39522  aomclem1  39532  aomclem6  39537  lnr2i  39594  hbtlem5  39606  hbt  39608  pwssfi  41184  rexanuz3  41239  choicefi  41339  fsneq  41345  suplesup  41483  xralrple2  41498  infxr  41511  infleinf  41516  xralrple4  41517  xralrple3  41518  xrralrecnnge  41538  supxrunb3  41548  supxrleubrnmpt  41555  unb2ltle  41565  suprleubrnmpt  41572  infxrgelbrnmpt  41606  supminfxr  41616  xrpnf  41638  islpcn  41796  limclner  41808  climd  41829  clim2d  41830  limsupmnflem  41877  limsupre3uzlem  41892  liminflelimsuplem  41932  xlimpnfxnegmnf  41971  xlimxrre  41988  xlimmnfvlem1  41989  xlimmnfv  41991  xlimpnfvlem1  41993  xlimpnfv  41995  climxlim2lem  42002  ioodvbdlimc1lem1  42092  ioodvbdlimc1lem2  42093  ioodvbdlimc2lem  42095  fourierdlem103  42371  fourierdlem104  42372  etransclem48  42444  saluncl  42479  subsaliuncllem  42517  sge0pnffigt  42555  omessle  42657  caragensplit  42659  omeunile  42664  hoidmvlelem2  42755  hoidmvlelem3  42756  hoidmvle  42759  vonvolmbllem  42819  vonvolmbl  42820  pimdecfgtioc  42870  smfpreimalt  42885  smfpreimaltf  42890  smfpreimale  42908  smfpreimagt  42915  smfpreimage  42935  smfmullem4  42946  smfinflem  42968  iccpartrn  43467  iccpartiun  43471  icceuelpart  43473  lidldomn1  44120  ply1mulgsumlem2  44369  lindslinindsimp2lem5  44445  lindslinindsimp2  44446  snlindsntor  44454  nn0sumshdiglemA  44607  nn0sumshdiglemB  44608  nn0sumshdig  44611
  Copyright terms: Public domain W3C validator