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

Theorem rspcva 2993
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 2991 . 2  |-  ( A  e.  B  ->  ( A. x  e.  B  ph 
->  ps ) )
32imp 419 1  |-  ( ( A  e.  B  /\  A. x  e.  B  ph )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1649    e. wcel 1717   A.wral 2649
This theorem is referenced by:  tfisi  4778  suppssov1  6241  caofinvl  6270  boxriin  7040  boxcutc  7041  marypha1lem  7373  marypha1  7374  supmo  7390  wemaplem2  7449  unwdomg  7485  noinfepOLD  7548  isinffi  7812  dfac9  7949  sornom  8090  fin23lem11  8130  fin1a2lem13  8225  axdc3lem2  8264  winalim2  8504  grothac  8638  nqereu  8739  infmrcl  9919  nnsub  9970  zextle  10275  xrsupsslem  10817  xrinfmsslem  10818  supxrunb1  10830  supxrunb2  10831  injresinjlem  11126  faclbnd4lem4  11514  rexuz3  12079  cau3lem  12085  caubnd2  12088  o1co  12307  climcn1  12312  incexclem  12543  dvdsext  12827  prdsbasprj  13621  mreintcl  13747  isacs2  13805  acsfiel  13806  isdrs2  14323  lubid  14366  acsdrsel  14520  isacs4lem  14521  isacs5lem  14522  acsdrscl  14523  acsficl  14524  mgmidmo  14620  gsumval2  14710  odeq  15115  gexid  15142  mplind  16489  cmpsublem  17384  cmpsub  17385  hauscmplem  17391  cmpfii  17394  ptpjcn  17564  isufil2  17861  ufileu  17872  cfiluweak  18246  cuspcvg  18252  lpbl  18423  lmmbr  19082  caussi  19121  evlslem1  19803  mdeglt  19855  deg1lt  19887  ply1divex  19926  plyco0  19978  dgrco  20060  emcllem7  20707  isppw2  20765  pntleme  21169  pntlemp  21171  nbcusgra  21338  uvtxnbgra  21368  wlkdvspthlem  21455  grpoidinvlem3  21642  grpoideu  21645  lnconi  23384  ishashinf  23997  kerf1hrm  24078  tpr2rico  24114  ofcfeqd2  24280  0elsiga  24293  sigaclci  24311  dya2icoseg2  24422  derangsn  24635  wfr3g  25279  frr3g  25304  fdc  26140  bndss  26186  isdrngo2  26265  divrngidl  26329  maxidlmax  26344  ismrcd1  26443  nacsfg  26450  isnacs3  26455  nacsfix  26457  mzpcl1  26477  mzpcl2  26478  mzpcong  26728  dnnumch1  26810  fnwe2lem2  26817  aomclem1  26820  aomclem4  26823  aomclem6  26825  lnr2i  26989  hbtlem5  27001  hbt  27003  frgraunss  27748  vdn0frgrav2  27777  vdgn0frgrav2  27778  vdn1frgrav2  27779  vdgn1frgrav2  27780  frgrancvvdeqlem4  27785  frgraregorufr  27805  cdleme0nex  30404  dihglblem2N  31409  hgmapvs  32009
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ral 2654  df-v 2901
  Copyright terms: Public domain W3C validator