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

Theorem rspcva 3186
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 3184 . 2  |-  ( A  e.  B  ->  ( A. x  e.  B  ph 
->  ps ) )
32imp 430 1  |-  ( ( A  e.  B  /\  A. x  e.  B  ph )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370    = wceq 1437    e. wcel 1870   A.wral 2782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ral 2787  df-v 3089
This theorem is referenced by:  rexraleqim  3203  fvn0ssdmfun  6028  fveqdmss  6032  fvcofneq  6045  caofinvl  6572  tfisi  6699  suppssov1  6958  wfr3g  7042  wfrlem17  7060  tfrlem1  7102  boxriin  7572  boxcutc  7573  marypha1lem  7953  marypha1  7954  supmo  7972  wemaplem2  8062  unwdomg  8099  isinffi  8425  dfac9  8564  sornom  8705  fin23lem11  8745  fin1a2lem13  8840  axdc3lem2  8879  winalim2  9120  grothac  9254  nqereu  9353  infmrclOLD  10593  nnsub  10648  zextle  11009  xrsupsslem  11592  xrinfmsslem  11593  supxrunb1  11605  supxrunb2  11606  injresinjlem  12021  ssnn0fi  12194  suppssfz  12203  faclbnd4lem4  12478  rexuz3  13390  cau3lem  13396  caubnd2  13399  o1co  13628  climcn1  13633  incexclem  13872  dvdsext  14334  cshwsidrepsw  15027  prdsbasprj  15329  mreintcl  15452  isacs2  15510  acsfiel  15511  initoeu1  15857  initoeu2  15862  termoeu1  15864  isdrs2  16135  lublecllem  16185  joinle  16211  meetle  16225  acsdrsel  16364  isacs4lem  16365  isacs5lem  16366  acsdrscl  16367  acsficl  16368  mgmidmo  16453  gsumval2  16474  mrcmndind  16564  symgfix2  17008  odeq  17141  gexid  17168  mplind  18660  evlslem1  18673  gsummoncoe1  18833  psgndiflemB  19099  mdetunilem1  19568  m2detleiblem3  19585  m2detleiblem4  19586  cpmatmcllem  19673  mp2pm2mplem4  19764  cayleyhamilton1  19847  cmpsublem  20345  cmpsub  20346  hauscmplem  20352  cmpfii  20355  ptpjcn  20557  isufil2  20854  ufileu  20865  isucn2  21225  cfiluweak  21241  cuspcvg  21247  lpbl  21449  lmmbr  22121  caussi  22160  mdeglt  22891  deg1lt  22923  ply1divex  22962  plyco0  23014  dgrco  23097  emcllem7  23792  isppw2  23905  pntleme  24309  pntlemp  24311  tglowdim2ln  24556  nbcusgra  25036  uvtxnbgra  25066  wlkdvspthlem  25182  clwwlkf  25367  rusgranumwlks  25529  frgraunss  25568  vdn0frgrav2  25596  vdgn0frgrav2  25597  vdn1frgrav2  25598  vdgn1frgrav2  25599  frgrancvvdeqlem4  25606  frgraregorufr  25626  extwwlkfablem1  25647  grpoidinvlem3  25779  grpoideu  25782  lnconi  27521  ishashinf  28217  rngurd  28390  tpr2rico  28557  esumiun  28754  ofcfeqd2  28761  0elsiga  28775  sigaclci  28793  dya2icoseg2  28939  signstfvneq0  29249  derangsn  29681  frr3g  30300  fwddifnp1  30717  poimirlem25  31668  poimirlem26  31669  poimirlem30  31673  poimirlem31  31674  poimirlem32  31675  heicant  31678  mblfinlem2  31681  ftc1anc  31728  fdc  31777  bndss  31821  isdrngo2  31900  divrngidl  31964  maxidlmax  31979  cdleme0nex  33564  dihglblem2N  34570  hgmapvs  35170  ismrcd1  35248  nacsfg  35255  isnacs3  35260  nacsfix  35262  mzpcl1  35279  mzpcl2  35280  mzpcong  35527  dnnumch1  35607  fnwe2lem2  35614  aomclem1  35617  aomclem4  35620  aomclem6  35622  lnr2i  35680  hbtlem5  35692  hbt  35694  pwssfi  37020  suplesup  37170  islpcn  37290  limclner  37303  cncfshift  37322  cncfperiod  37327  ioodvbdlimc1lem1  37374  ioodvbdlimc1lem2  37375  ioodvbdlimc2lem  37377  fourierdlem103  37640  fourierdlem104  37641  etransclem48  37713  salunicl  37723  saluncl  37724  saldifcl  37726  sge0pnffigt  37771  meadjuni  37803  omessle  37827  caragensplit  37829  omeunile  37834  iccpartimp  38120  iccpartrn  38133  iccpartiun  38137  icceuelpart  38139  reuccatpfxs1  38364  lidldomn1  38678  ply1mulgsumlem2  38938  lindslinindsimp2lem5  39014  lindslinindsimp2  39015  snlindsntor  39023  nn0sumshdiglemA  39190  nn0sumshdiglemB  39191  nn0sumshdig  39194
  Copyright terms: Public domain W3C validator