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

Theorem rexlimivw 2930
Description: Weaker version of rexlimiv 2927. (Contributed by FL, 19-Sep-2011.)
Hypothesis
Ref Expression
rexlimivw.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
rexlimivw  |-  ( E. x  e.  A  ph  ->  ps )
Distinct variable group:    ps, x
Allowed substitution hints:    ph( x)    A( x)

Proof of Theorem rexlimivw
StepHypRef Expression
1 rexlimivw.1 . . 3  |-  ( ph  ->  ps )
21a1i 11 . 2  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
32rexlimiv 2927 1  |-  ( E. x  e.  A  ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1802   E.wrex 2792
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1598  df-ral 2796  df-rex 2797
This theorem is referenced by:  r19.29_2a  2985  sbcreu  3398  eliun  4316  reusv3i  4640  reusv7OLD  4645  elrnmptg  5238  fvelrnb  5901  fvelimab  5910  iinpreima  5998  fmpt  6033  fliftfun  6191  elrnmpt2  6396  ovelrn  6432  onuninsuci  6656  fun11iun  6741  releldm2  6831  tfrlem4  7046  iiner  7381  elixpsn  7506  isfi  7537  card2on  7978  tz9.12lem1  8203  rankwflemb  8209  rankxpsuc  8298  scott0  8302  isnum2  8324  cardiun  8361  cardalephex  8469  dfac5lem4  8505  dfac12k  8525  cflim2  8641  cfss  8643  cfslb2n  8646  enfin2i  8699  fin23lem30  8720  itunitc  8799  axdc3lem2  8829  iundom2g  8913  pwcfsdom  8956  cfpwsdom  8957  tskr1om2  9144  genpelv  9376  prlem934  9409  suplem1pr  9428  supexpr  9430  supsrlem  9486  supsr  9487  fimaxre3  10493  iswrd  12524  caurcvgr  13470  caurcvg  13473  caucvg  13475  vdwapval  14363  restsspw  14701  mreunirn  14870  brssc  15055  arwhoma  15241  gexcl3  16476  dvdsr  17163  lspsnel  17517  lspprel  17608  ellspd  18703  ellspdOLD  18704  iincld  19406  ssnei  19477  neindisj2  19490  neitr  19547  lecldbas  19586  tgcnp  19620  cncnp2  19648  lmmo  19747  is2ndc  19813  fbfinnfr  20208  fbunfip  20236  filunirn  20249  fbflim2  20344  flimcls  20352  hauspwpwf1  20354  flftg  20363  isfcls  20376  fclsbas  20388  isfcf  20401  ustfilxp  20581  ustbas  20596  restutop  20606  ucnima  20650  xmetunirn  20706  metss  20877  metrest  20893  restmetu  20956  qdensere  21143  elpi1  21411  lmmbr  21563  caun0  21586  nulmbl2  21813  itg2l  22002  aannenlem2  22590  taylfval  22619  ulmcl  22641  ulmpm  22643  ulmss  22657  tglnunirn  23800  ishpg  23993  3v3e3cycl1  24509  iseupa  24830  frgrancvvdeqlem4  24898  frg2wotn0  24921  usgreghash2spot  24934  hhcms  25985  hhsscms  26060  occllem  26086  occl  26087  chscllem2  26421  rabfmpunirn  27356  rhmdvdsr  27674  kerunit  27679  tpr2rico  27760  gsumesum  27933  esumcst  27937  esumfsup  27942  esumpcvgval  27950  esumcvg  27958  sigaclcuni  27984  mbfmfun  28091  dya2icoseg2  28115  rellyscon  28562  cvmliftlem15  28609  orderseqlem  29300  nofun  29377  norn  29379  dfrdg4  29568  brcolinear2  29676  brcolinear  29677  ellines  29770  volsupnfl  30027  unirep  30171  filbcmb  30199  rngunsnply  31091  usgra2pth  32188  bnj66  33625  bnj517  33650  islshpkrN  34547  ispointN  35168  pmapglbx  35195
  Copyright terms: Public domain W3C validator