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

Theorem rexlimivw 2826
Description: Weaker version of rexlimiv 2824. (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 2824 1  |-  ( E. x  e.  A  ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725   E.wrex 2706
This theorem is referenced by:  r19.29_2a  2852  eliun  4097  reusv3i  4730  reusv7OLD  4735  onuninsuci  4820  elrnmptg  5120  fun11iun  5695  fvelrnb  5774  fvelimab  5782  iinpreima  5860  fmpt  5890  fliftfun  6034  elrnmpt2  6183  ovelrn  6222  releldm2  6397  tfrlem4  6640  abianfp  6716  iiner  6976  elixpsn  7101  isfi  7131  card2on  7522  tz9.12lem1  7713  rankwflemb  7719  rankxpsuc  7806  scott0  7810  isnum2  7832  cardiun  7869  cardalephex  7971  dfac5lem4  8007  dfac12k  8027  cflim2  8143  cfss  8145  cfslb2n  8148  enfin2i  8201  fin23lem30  8222  itunitc  8301  axdc3lem2  8331  iundom2g  8415  pwcfsdom  8458  cfpwsdom  8459  tskr1om2  8643  gruiun  8674  genpelv  8877  prlem934  8910  suplem1pr  8929  supexpr  8931  supsrlem  8986  supsr  8987  fimaxre3  9957  iswrd  11729  caurcvgr  12467  caurcvg  12470  caucvg  12472  vdwapval  13341  restsspw  13659  mreunirn  13826  brssc  14014  arwhoma  14200  gexcl3  15221  dvdsr  15751  lspsnel  16079  lspprel  16166  iincld  17103  ssnei  17174  neindisj2  17187  neitr  17244  lecldbas  17283  tgcnp  17317  cncnp2  17345  lmmo  17444  is2ndc  17509  fbfinnfr  17873  fbunfip  17901  filunirn  17914  fbflim2  18009  flimcls  18017  hauspwpwf1  18019  flftg  18028  isfcls  18041  fclsbas  18053  isfcf  18066  ustfilxp  18242  ustbas  18257  restutop  18267  ucnima  18311  xmetunirn  18367  metss  18538  metrest  18554  restmetu  18617  qdensere  18804  elpi1  19070  lmmbr  19211  caun0  19234  nulmbl2  19431  itg2l  19621  aannenlem2  20246  taylfval  20275  ulmcl  20297  ulmpm  20299  ulmss  20313  3v3e3cycl1  21631  iseupa  21687  hhcms  22705  hhsscms  22779  occllem  22805  occl  22806  chscllem2  23140  rabfmpunirn  24065  rhmdvdsr  24256  kerunit  24261  tpr2rico  24310  gsumesum  24451  esumcst  24455  esumfsup  24460  esumpcvgval  24468  esumcvg  24476  sigaclcuni  24501  mbfmfun  24604  dya2icoseg2  24628  rellyscon  24938  cvmliftlem15  24985  orderseqlem  25527  nofun  25604  norn  25606  dfrdg4  25795  brcolinear2  25992  brcolinear  25993  ellines  26086  volsupnfl  26251  unirep  26414  filbcmb  26442  ellspd  27231  rngunsnply  27355  usgra2pth  28311  frgrancvvdeqlem4  28422  frg2wotn0  28445  usgreghash2spot  28458  bnj66  29231  bnj517  29256  islshpkrN  29918  ispointN  30539  pmapglbx  30566
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554  df-ral 2710  df-rex 2711
  Copyright terms: Public domain W3C validator