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

Theorem rspcva 3010
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 3008 . 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 1721   A.wral 2666
This theorem is referenced by:  tfisi  4797  suppssov1  6261  caofinvl  6290  boxriin  7063  boxcutc  7064  marypha1lem  7396  marypha1  7397  supmo  7413  wemaplem2  7472  unwdomg  7508  noinfepOLD  7571  isinffi  7835  dfac9  7972  sornom  8113  fin23lem11  8153  fin1a2lem13  8248  axdc3lem2  8287  winalim2  8527  grothac  8661  nqereu  8762  infmrcl  9943  nnsub  9994  zextle  10299  xrsupsslem  10841  xrinfmsslem  10842  supxrunb1  10854  supxrunb2  10855  injresinjlem  11154  faclbnd4lem4  11542  rexuz3  12107  cau3lem  12113  caubnd2  12116  o1co  12335  climcn1  12340  incexclem  12571  dvdsext  12855  prdsbasprj  13649  mreintcl  13775  isacs2  13833  acsfiel  13834  isdrs2  14351  lubid  14394  acsdrsel  14548  isacs4lem  14549  isacs5lem  14550  acsdrscl  14551  acsficl  14552  mgmidmo  14648  gsumval2  14738  odeq  15143  gexid  15170  mplind  16517  cmpsublem  17416  cmpsub  17417  hauscmplem  17423  cmpfii  17426  ptpjcn  17596  isufil2  17893  ufileu  17904  cfiluweak  18278  cuspcvg  18284  lpbl  18486  lmmbr  19164  caussi  19203  evlslem1  19889  mdeglt  19941  deg1lt  19973  ply1divex  20012  plyco0  20064  dgrco  20146  emcllem7  20793  isppw2  20851  pntleme  21255  pntlemp  21257  nbcusgra  21425  uvtxnbgra  21455  wlkdvspthlem  21560  grpoidinvlem3  21747  grpoideu  21750  lnconi  23489  ishashinf  24112  kerf1hrm  24215  tpr2rico  24263  ofcfeqd2  24437  0elsiga  24450  sigaclci  24468  dya2icoseg2  24581  derangsn  24809  wfr3g  25469  frr3g  25494  mblfinlem  26143  fdc  26339  bndss  26385  isdrngo2  26464  divrngidl  26528  maxidlmax  26543  ismrcd1  26642  nacsfg  26649  isnacs3  26654  nacsfix  26656  mzpcl1  26676  mzpcl2  26677  mzpcong  26927  dnnumch1  27009  fnwe2lem2  27016  aomclem1  27019  aomclem4  27022  aomclem6  27024  lnr2i  27188  hbtlem5  27200  hbt  27202  frgraunss  28099  vdn0frgrav2  28128  vdgn0frgrav2  28129  vdn1frgrav2  28130  vdgn1frgrav2  28131  frgrancvvdeqlem4  28136  frgraregorufr  28156  cdleme0nex  30772  dihglblem2N  31777  hgmapvs  32377
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ral 2671  df-v 2918
  Copyright terms: Public domain W3C validator