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

Theorem rspcva 3205
Description: Restricted specialization, using implicit substitution. (Contributed by NM, 13-Sep-2005.)
Hypothesis
Ref Expression
rspcv.1  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
rspcva  |-  ( ( A  e.  B  /\  A. x  e.  B  ph )  ->  ps )
Distinct variable groups:    x, A    x, B    ps, x
Allowed substitution hint:    ph( x)

Proof of Theorem rspcva
StepHypRef Expression
1 rspcv.1 . . 3  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
21rspcv 3203 . 2  |-  ( A  e.  B  ->  ( A. x  e.  B  ph 
->  ps ) )
32imp 429 1  |-  ( ( A  e.  B  /\  A. x  e.  B  ph )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1374    e. wcel 1762   A.wral 2807
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ral 2812  df-v 3108
This theorem is referenced by:  rexraleqim  3222  fvcofneq  6020  suppssov1OLD  6507  caofinvl  6542  tfisi  6664  suppfnss  6915  suppssov1  6922  tfrlem1  7035  boxriin  7501  boxcutc  7502  marypha1lem  7882  marypha1  7883  supmo  7901  wemaplem2  7961  unwdomg  7999  noinfepOLD  8066  isinffi  8362  dfac9  8505  sornom  8646  fin23lem11  8686  fin1a2lem13  8781  axdc3lem2  8820  winalim2  9063  grothac  9197  nqereu  9296  infmrcl  10511  nnsub  10563  zextle  10923  xrsupsslem  11487  xrinfmsslem  11488  supxrunb1  11500  supxrunb2  11501  injresinjlem  11882  ssnn0fi  12050  suppssfz  12056  faclbnd4lem4  12329  reuccats1lem  12655  rexuz3  13130  cau3lem  13136  caubnd2  13139  o1co  13358  climcn1  13363  incexclem  13600  dvdsext  13885  cshwsidrepsw  14425  prdsbasprj  14716  mreintcl  14839  isacs2  14897  acsfiel  14898  isdrs2  15415  lublecllem  15464  joinle  15490  meetle  15504  acsdrsel  15643  isacs4lem  15644  isacs5lem  15645  acsdrscl  15646  acsficl  15647  mgmidmo  15724  mrcmndind  15800  gsumval2  15819  symgfix2  16229  odeq  16363  gexid  16390  mplind  17931  evlslem1  17948  cply1mul  18099  gsummoncoe1  18110  psgndiflemB  18396  mvmumamul1  18816  mdetunilem1  18874  m2detleiblem3  18891  m2detleiblem4  18892  cpmatmcllem  18979  mp2pm2mplem4  19070  cayleyhamilton1  19153  cmpsublem  19658  cmpsub  19659  hauscmplem  19665  cmpfii  19668  ptpjcn  19840  isufil2  20137  ufileu  20148  cfiluweak  20526  cuspcvg  20532  lpbl  20734  lmmbr  21425  caussi  21464  mdeglt  22193  deg1lt  22226  ply1divex  22265  plyco0  22317  dgrco  22399  emcllem7  23052  isppw2  23110  pntleme  23514  pntlemp  23516  tglowdim2ln  23738  nbcusgra  24125  uvtxnbgra  24155  wlkdvspthlem  24271  clwwlkf  24456  clwwisshclwwlem1  24467  clwlkf1clwwlklem  24511  nbhashnn0  24576  vdiscusgra  24583  rusgraprop4  24606  rusgranumwwlkl1  24608  rusgranumwlks  24618  frgraunss  24657  vdn0frgrav2  24686  vdgn0frgrav2  24687  vdn1frgrav2  24688  vdgn1frgrav2  24689  usgn0fidegnn0  24692  frgrancvvdeqlem4  24696  frgraregorufr  24716  extwwlkfablem1  24737  numclwwlk1  24761  grpoidinvlem3  24870  grpoideu  24873  lnconi  26614  ishashinf  27260  tpr2rico  27516  ofcfeqd2  27726  0elsiga  27740  sigaclci  27758  dya2icoseg2  27875  derangsn  28240  wfr3g  28905  frr3g  28949  heicant  29613  mblfinlem2  29616  ftc1anc  29662  fdc  29828  bndss  29872  isdrngo2  29951  divrngidl  30015  maxidlmax  30030  ismrcd1  30221  nacsfg  30228  isnacs3  30233  nacsfix  30235  mzpcl1  30252  mzpcl2  30253  mzpcong  30501  dnnumch1  30583  fnwe2lem2  30590  aomclem1  30593  aomclem4  30596  aomclem6  30598  lnr2i  30658  hbtlem5  30670  hbt  30672  islpcn  31136  limclner  31148  cncfshift  31167  cncfperiod  31172  icocncflimc  31183  ioodvbdlimc1lem1  31216  ioodvbdlimc1lem2  31217  ioodvbdlimc2lem  31219  fourierdlem45  31407  fourierdlem103  31465  fourierdlem104  31466  ply1mulgsumlem2  31935  lindslinindsimp2lem5  32011  lindslinindsimp2  32012  snlindsntor  32020  cdleme0nex  34961  dihglblem2N  35966  hgmapvs  36566
  Copyright terms: Public domain W3C validator