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

Theorem rspcva 3194
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 3192 . 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 1383    e. wcel 1804   A.wral 2793
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ral 2798  df-v 3097
This theorem is referenced by:  rexraleqim  3211  fvn0ssdmfun  6007  fveqdmss  6011  fvcofneq  6024  suppssov1OLD  6517  caofinvl  6552  tfisi  6678  suppssov1  6934  tfrlem1  7047  boxriin  7513  boxcutc  7514  marypha1lem  7895  marypha1  7896  supmo  7914  wemaplem2  7975  unwdomg  8013  noinfepOLD  8080  isinffi  8376  dfac9  8519  sornom  8660  fin23lem11  8700  fin1a2lem13  8795  axdc3lem2  8834  winalim2  9077  grothac  9211  nqereu  9310  infmrcl  10528  nnsub  10580  zextle  10942  xrsupsslem  11507  xrinfmsslem  11508  supxrunb1  11520  supxrunb2  11521  injresinjlem  11904  ssnn0fi  12073  suppssfz  12079  faclbnd4lem4  12353  rexuz3  13160  cau3lem  13166  caubnd2  13169  o1co  13388  climcn1  13393  incexclem  13627  dvdsext  13914  cshwsidrepsw  14455  prdsbasprj  14746  mreintcl  14869  isacs2  14927  acsfiel  14928  isdrs2  15442  lublecllem  15492  joinle  15518  meetle  15532  acsdrsel  15671  isacs4lem  15672  isacs5lem  15673  acsdrscl  15674  acsficl  15675  mgmidmo  15760  gsumval2  15781  mrcmndind  15871  symgfix2  16315  odeq  16448  gexid  16475  mplind  18041  evlslem1  18058  gsummoncoe1  18220  psgndiflemB  18509  mdetunilem1  18987  m2detleiblem3  19004  m2detleiblem4  19005  cpmatmcllem  19092  mp2pm2mplem4  19183  cayleyhamilton1  19266  cmpsublem  19772  cmpsub  19773  hauscmplem  19779  cmpfii  19782  ptpjcn  19985  isufil2  20282  ufileu  20293  isucn2  20655  cfiluweak  20671  cuspcvg  20677  lpbl  20879  lmmbr  21570  caussi  21609  mdeglt  22338  deg1lt  22371  ply1divex  22410  plyco0  22462  dgrco  22544  emcllem7  23203  isppw2  23261  pntleme  23665  pntlemp  23667  tglowdim2ln  23904  nbcusgra  24335  uvtxnbgra  24365  wlkdvspthlem  24481  clwwlkf  24666  rusgranumwlks  24828  frgraunss  24867  vdn0frgrav2  24895  vdgn0frgrav2  24896  vdn1frgrav2  24897  vdgn1frgrav2  24898  frgrancvvdeqlem4  24905  frgraregorufr  24925  extwwlkfablem1  24946  grpoidinvlem3  25080  grpoideu  25083  lnconi  26824  ishashinf  27478  rngurd  27651  tpr2rico  27767  ofcfeqd2  27973  0elsiga  27987  sigaclci  28005  dya2icoseg2  28122  signstfvneq0  28402  derangsn  28487  wfr3g  29317  frr3g  29361  heicant  30024  mblfinlem2  30027  ftc1anc  30073  fdc  30213  bndss  30257  isdrngo2  30336  divrngidl  30400  maxidlmax  30415  ismrcd1  30605  nacsfg  30612  isnacs3  30617  nacsfix  30619  mzpcl1  30636  mzpcl2  30637  mzpcong  30885  dnnumch1  30965  fnwe2lem2  30972  aomclem1  30975  aomclem4  30978  aomclem6  30980  lnr2i  31040  hbtlem5  31052  hbt  31054  islpcn  31553  limclner  31565  cncfshift  31583  cncfperiod  31588  ioodvbdlimc1lem1  31632  ioodvbdlimc1lem2  31633  ioodvbdlimc2lem  31635  fourierdlem103  31881  fourierdlem104  31882  lidldomn1  32437  ply1mulgsumlem2  32722  lindslinindsimp2lem5  32798  lindslinindsimp2  32799  snlindsntor  32807  cdleme0nex  35755  dihglblem2N  36761  hgmapvs  37361
  Copyright terms: Public domain W3C validator