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

Theorem rspcva 2895
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 2893 . 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 1632    e. wcel 1696   A.wral 2556
This theorem is referenced by:  tfisi  4665  suppssov1  6091  caofinvl  6120  boxriin  6874  boxcutc  6875  marypha1lem  7202  marypha1  7203  supmo  7219  wemaplem2  7278  unwdomg  7314  noinfepOLD  7377  isinffi  7641  dfac9  7778  sornom  7919  fin23lem11  7959  fin1a2lem13  8054  axdc3lem2  8093  winalim2  8334  grothac  8468  nqereu  8569  infmrcl  9749  nnsub  9800  zextle  10101  xrsupsslem  10641  xrinfmsslem  10642  supxrunb1  10654  supxrunb2  10655  faclbnd4lem4  11325  rexuz3  11848  cau3lem  11854  caubnd2  11857  o1co  12076  climcn1  12081  incexclem  12311  dvdsext  12595  prdsbasprj  13387  mreintcl  13513  isacs2  13571  acsfiel  13572  isdrs2  14089  lubid  14132  acsdrsel  14286  isacs4lem  14287  isacs5lem  14288  acsdrscl  14289  acsficl  14290  mgmidmo  14386  gsumval2  14476  odeq  14881  gexid  14908  mplind  16259  cmpsublem  17142  cmpsub  17143  hauscmplem  17149  cmpfii  17152  ptpjcn  17321  isufil2  17619  ufileu  17630  lpbl  18065  lmmbr  18700  caussi  18739  evlslem1  19415  mdeglt  19467  deg1lt  19499  ply1divex  19538  plyco0  19590  dgrco  19672  emcllem7  20311  isppw2  20369  pntleme  20773  pntlemp  20775  grpoidinvlem3  20889  grpoideu  20892  lnconi  22629  tpr2rico  23311  ishashinf  23404  ofcfeqd2  23477  0elsiga  23490  sigaclci  23508  derangsn  23716  wfr3g  24326  frr3g  24351  srefwref  25170  domintrefc  25228  rzrlzreq  25439  limptlimpr2lem1  25677  pgapspf  26155  isig12  26167  fdc  26558  bndss  26613  isdrngo2  26692  divrngidl  26756  maxidlmax  26771  ismrcd1  26876  nacsfg  26883  isnacs3  26888  nacsfix  26890  mzpcl1  26910  mzpcl2  26911  mzpcong  27162  dnnumch1  27244  fnwe2lem2  27251  aomclem1  27254  aomclem4  27257  aomclem6  27259  lnr2i  27423  hbtlem5  27435  hbt  27437  injresinjlem  28214  nbcusgra  28298  uvtxnbgra  28306  cusgrauvtx  28309  wlkdvspthlem  28365  usgrcyclnl1  28386  cdleme0nex  31101  dihglblem2N  32106  hgmapvs  32706
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-v 2803
  Copyright terms: Public domain W3C validator