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

Theorem rspcva 3133
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 3131 . 2  |-  ( A  e.  B  ->  ( A. x  e.  B  ph 
->  ps ) )
32imp 427 1  |-  ( ( A  e.  B  /\  A. x  e.  B  ph )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367    = wceq 1399    e. wcel 1826   A.wral 2732
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ral 2737  df-v 3036
This theorem is referenced by:  rexraleqim  3150  fvn0ssdmfun  5924  fveqdmss  5928  fvcofneq  5941  suppssov1OLD  6431  caofinvl  6466  tfisi  6592  suppssov1  6850  tfrlem1  6963  boxriin  7430  boxcutc  7431  marypha1lem  7808  marypha1  7809  supmo  7826  wemaplem2  7887  unwdomg  7925  isinffi  8286  dfac9  8429  sornom  8570  fin23lem11  8610  fin1a2lem13  8705  axdc3lem2  8744  winalim2  8985  grothac  9119  nqereu  9218  infmrcl  10438  nnsub  10491  zextle  10853  xrsupsslem  11419  xrinfmsslem  11420  supxrunb1  11432  supxrunb2  11433  injresinjlem  11824  ssnn0fi  11997  suppssfz  12003  faclbnd4lem4  12276  rexuz3  13183  cau3lem  13189  caubnd2  13192  o1co  13411  climcn1  13416  incexclem  13650  dvdsext  14039  cshwsidrepsw  14580  prdsbasprj  14879  mreintcl  15002  isacs2  15060  acsfiel  15061  initoeu1  15407  initoeu2  15412  termoeu1  15414  isdrs2  15685  lublecllem  15735  joinle  15761  meetle  15775  acsdrsel  15914  isacs4lem  15915  isacs5lem  15916  acsdrscl  15917  acsficl  15918  mgmidmo  16003  gsumval2  16024  mrcmndind  16114  symgfix2  16558  odeq  16691  gexid  16718  mplind  18280  evlslem1  18297  gsummoncoe1  18459  psgndiflemB  18727  mdetunilem1  19199  m2detleiblem3  19216  m2detleiblem4  19217  cpmatmcllem  19304  mp2pm2mplem4  19395  cayleyhamilton1  19478  cmpsublem  19985  cmpsub  19986  hauscmplem  19992  cmpfii  19995  ptpjcn  20197  isufil2  20494  ufileu  20505  isucn2  20867  cfiluweak  20883  cuspcvg  20889  lpbl  21091  lmmbr  21782  caussi  21821  mdeglt  22550  deg1lt  22583  ply1divex  22622  plyco0  22674  dgrco  22757  emcllem7  23448  isppw2  23506  pntleme  23910  pntlemp  23912  tglowdim2ln  24152  nbcusgra  24584  uvtxnbgra  24614  wlkdvspthlem  24730  clwwlkf  24915  rusgranumwlks  25077  frgraunss  25116  vdn0frgrav2  25144  vdgn0frgrav2  25145  vdn1frgrav2  25146  vdgn1frgrav2  25147  frgrancvvdeqlem4  25154  frgraregorufr  25174  extwwlkfablem1  25195  grpoidinvlem3  25325  grpoideu  25328  lnconi  27068  ishashinf  27759  rngurd  27932  tpr2rico  28048  esumiun  28242  ofcfeqd2  28249  0elsiga  28263  sigaclci  28281  dya2icoseg2  28405  signstfvneq0  28712  derangsn  28803  wfr3g  29507  frr3g  29551  heicant  30214  mblfinlem2  30217  ftc1anc  30264  fdc  30404  bndss  30448  isdrngo2  30527  divrngidl  30591  maxidlmax  30606  ismrcd1  30796  nacsfg  30803  isnacs3  30808  nacsfix  30810  mzpcl1  30827  mzpcl2  30828  mzpcong  31075  dnnumch1  31156  fnwe2lem2  31163  aomclem1  31166  aomclem4  31169  aomclem6  31171  lnr2i  31233  hbtlem5  31245  hbt  31247  islpcn  31811  limclner  31823  cncfshift  31842  cncfperiod  31847  ioodvbdlimc1lem1  31894  ioodvbdlimc1lem2  31895  ioodvbdlimc2lem  31897  fourierdlem103  32158  fourierdlem104  32159  etransclem48  32231  reuccatpfxs1  32609  lidldomn1  32927  ply1mulgsumlem2  33187  lindslinindsimp2lem5  33263  lindslinindsimp2  33264  snlindsntor  33272  nn0sumshdiglemA  33440  nn0sumshdiglemB  33441  nn0sumshdig  33444  cdleme0nex  36428  dihglblem2N  37434  hgmapvs  38034
  Copyright terms: Public domain W3C validator