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

Theorem rexlimivw 2941
Description: Weaker version of rexlimiv 2939. (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 2939 1  |-  ( E. x  e.  A  ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1758   E.wrex 2799
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-12 1794
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-nf 1591  df-ral 2803  df-rex 2804
This theorem is referenced by:  r19.29_2a  2968  sbcreu  3379  eliun  4282  reusv3i  4606  reusv7OLD  4611  elrnmptg  5196  fvelrnb  5847  fvelimab  5855  iinpreima  5941  fmpt  5972  fliftfun  6113  elrnmpt2  6312  ovelrn  6348  onuninsuci  6560  fun11iun  6646  releldm2  6733  tfrlem4  6947  iiner  7281  elixpsn  7411  isfi  7442  card2on  7879  tz9.12lem1  8104  rankwflemb  8110  rankxpsuc  8199  scott0  8203  isnum2  8225  cardiun  8262  cardalephex  8370  dfac5lem4  8406  dfac12k  8426  cflim2  8542  cfss  8544  cfslb2n  8547  enfin2i  8600  fin23lem30  8621  itunitc  8700  axdc3lem2  8730  iundom2g  8814  pwcfsdom  8857  cfpwsdom  8858  tskr1om2  9045  gruiun  9076  genpelv  9279  prlem934  9312  suplem1pr  9331  supexpr  9333  supsrlem  9388  supsr  9389  fimaxre3  10389  iswrd  12354  caurcvgr  13268  caurcvg  13271  caucvg  13273  vdwapval  14151  restsspw  14488  mreunirn  14657  brssc  14845  arwhoma  15031  gexcl3  16206  dvdsr  16860  lspsnel  17206  lspprel  17297  ellspd  18354  ellspdOLD  18355  iincld  18774  ssnei  18845  neindisj2  18858  neitr  18915  lecldbas  18954  tgcnp  18988  cncnp2  19016  lmmo  19115  is2ndc  19181  fbfinnfr  19545  fbunfip  19573  filunirn  19586  fbflim2  19681  flimcls  19689  hauspwpwf1  19691  flftg  19700  isfcls  19713  fclsbas  19725  isfcf  19738  ustfilxp  19918  ustbas  19933  restutop  19943  ucnima  19987  xmetunirn  20043  metss  20214  metrest  20230  restmetu  20293  qdensere  20480  elpi1  20748  lmmbr  20900  caun0  20923  nulmbl2  21150  itg2l  21339  aannenlem2  21927  taylfval  21956  ulmcl  21978  ulmpm  21980  ulmss  21994  tglnunirn  23117  3v3e3cycl1  23681  iseupa  23737  hhcms  24756  hhsscms  24831  occllem  24857  occl  24858  chscllem2  25192  rabfmpunirn  26118  rhmdvdsr  26430  kerunit  26435  tpr2rico  26486  gsumesum  26654  esumcst  26658  esumfsup  26663  esumpcvgval  26671  esumcvg  26679  sigaclcuni  26705  mbfmfun  26812  dya2icoseg2  26836  rellyscon  27283  cvmliftlem15  27330  orderseqlem  27856  nofun  27933  norn  27935  dfrdg4  28124  brcolinear2  28232  brcolinear  28233  ellines  28326  volsupnfl  28583  unirep  28753  filbcmb  28781  rngunsnply  29677  usgra2pth  30448  frgrancvvdeqlem4  30773  frg2wotn0  30796  usgreghash2spot  30809  bnj66  32170  bnj517  32195  islshpkrN  33088  ispointN  33709  pmapglbx  33736
  Copyright terms: Public domain W3C validator