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

Theorem rexlimivw 2832
Description: Weaker version of rexlimiv 2830. (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 2830 1  |-  ( E. x  e.  A  ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   E.wrex 2711
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-12 1792
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-ral 2715  df-rex 2716
This theorem is referenced by:  r19.29_2a  2859  sbcreu  3268  eliun  4170  reusv3i  4494  reusv7OLD  4499  elrnmptg  5084  fvelrnb  5734  fvelimab  5742  iinpreima  5828  fmpt  5859  fliftfun  6000  elrnmpt2  6198  ovelrn  6234  onuninsuci  6446  fun11iun  6532  releldm2  6619  tfrlem4  6830  iiner  7164  elixpsn  7294  isfi  7325  card2on  7761  tz9.12lem1  7986  rankwflemb  7992  rankxpsuc  8081  scott0  8085  isnum2  8107  cardiun  8144  cardalephex  8252  dfac5lem4  8288  dfac12k  8308  cflim2  8424  cfss  8426  cfslb2n  8429  enfin2i  8482  fin23lem30  8503  itunitc  8582  axdc3lem2  8612  iundom2g  8696  pwcfsdom  8739  cfpwsdom  8740  tskr1om2  8927  gruiun  8958  genpelv  9161  prlem934  9194  suplem1pr  9213  supexpr  9215  supsrlem  9270  supsr  9271  fimaxre3  10271  iswrd  12229  caurcvgr  13143  caurcvg  13146  caucvg  13148  vdwapval  14026  restsspw  14362  mreunirn  14531  brssc  14719  arwhoma  14905  gexcl3  16077  dvdsr  16726  lspsnel  17061  lspprel  17152  ellspd  18205  ellspdOLD  18206  iincld  18618  ssnei  18689  neindisj2  18702  neitr  18759  lecldbas  18798  tgcnp  18832  cncnp2  18860  lmmo  18959  is2ndc  19025  fbfinnfr  19389  fbunfip  19417  filunirn  19430  fbflim2  19525  flimcls  19533  hauspwpwf1  19535  flftg  19544  isfcls  19557  fclsbas  19569  isfcf  19582  ustfilxp  19762  ustbas  19777  restutop  19787  ucnima  19831  xmetunirn  19887  metss  20058  metrest  20074  restmetu  20137  qdensere  20324  elpi1  20592  lmmbr  20744  caun0  20767  nulmbl2  20993  itg2l  21182  aannenlem2  21770  taylfval  21799  ulmcl  21821  ulmpm  21823  ulmss  21837  tglnunirn  22957  3v3e3cycl1  23481  iseupa  23537  hhcms  24556  hhsscms  24631  occllem  24657  occl  24658  chscllem2  24992  rabfmpunirn  25919  rhmdvdsr  26237  kerunit  26242  tpr2rico  26294  gsumesum  26462  esumcst  26466  esumfsup  26471  esumpcvgval  26479  esumcvg  26487  sigaclcuni  26513  mbfmfun  26621  dya2icoseg2  26645  rellyscon  27092  cvmliftlem15  27139  orderseqlem  27664  nofun  27741  norn  27743  dfrdg4  27932  brcolinear2  28040  brcolinear  28041  ellines  28134  volsupnfl  28389  unirep  28559  filbcmb  28587  rngunsnply  29483  usgra2pth  30254  frgrancvvdeqlem4  30579  frg2wotn0  30602  usgreghash2spot  30615  bnj66  31740  bnj517  31765  islshpkrN  32605  ispointN  33226  pmapglbx  33253
  Copyright terms: Public domain W3C validator