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

Theorem rspcva 2882
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 2880 . 2  |-  ( A  e.  B  ->  ( A. x  e.  B  ph 
->  ps ) )
32imp 418 1  |-  ( ( A  e.  B  /\  A. x  e.  B  ph )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1623    e. wcel 1684   A.wral 2543
This theorem is referenced by:  tfisi  4649  suppssov1  6075  caofinvl  6104  boxriin  6858  boxcutc  6859  marypha1lem  7186  marypha1  7187  supmo  7203  wemaplem2  7262  unwdomg  7298  noinfepOLD  7361  isinffi  7625  dfac9  7762  sornom  7903  fin23lem11  7943  fin1a2lem13  8038  axdc3lem2  8077  winalim2  8318  grothac  8452  nqereu  8553  infmrcl  9733  nnsub  9784  zextle  10085  xrsupsslem  10625  xrinfmsslem  10626  supxrunb1  10638  supxrunb2  10639  faclbnd4lem4  11309  rexuz3  11832  cau3lem  11838  caubnd2  11841  o1co  12060  climcn1  12065  incexclem  12295  dvdsext  12579  prdsbasprj  13371  mreintcl  13497  isacs2  13555  acsfiel  13556  isdrs2  14073  lubid  14116  acsdrsel  14270  isacs4lem  14271  isacs5lem  14272  acsdrscl  14273  acsficl  14274  mgmidmo  14370  gsumval2  14460  odeq  14865  gexid  14892  mplind  16243  cmpsublem  17126  cmpsub  17127  hauscmplem  17133  cmpfii  17136  ptpjcn  17305  isufil2  17603  ufileu  17614  lpbl  18049  lmmbr  18684  caussi  18723  evlslem1  19399  mdeglt  19451  deg1lt  19483  ply1divex  19522  plyco0  19574  dgrco  19656  emcllem7  20295  isppw2  20353  pntleme  20757  pntlemp  20759  grpoidinvlem3  20873  grpoideu  20876  lnconi  22613  tpr2rico  23296  ishashinf  23389  ofcfeqd2  23462  0elsiga  23475  sigaclci  23493  derangsn  23701  wfr3g  24255  frr3g  24280  srefwref  25067  domintrefc  25125  rzrlzreq  25336  limptlimpr2lem1  25574  pgapspf  26052  isig12  26064  fdc  26455  bndss  26510  isdrngo2  26589  divrngidl  26653  maxidlmax  26668  ismrcd1  26773  nacsfg  26780  isnacs3  26785  nacsfix  26787  mzpcl1  26807  mzpcl2  26808  mzpcong  27059  dnnumch1  27141  fnwe2lem2  27148  aomclem1  27151  aomclem4  27154  aomclem6  27156  lnr2i  27320  hbtlem5  27332  hbt  27334  nbcusgra  28159  uvtxnbgra  28165  cusgrauvtx  28168  cdleme0nex  30479  dihglblem2N  31484  hgmapvs  32084
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-v 2790
  Copyright terms: Public domain W3C validator