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

Theorem rexlimivw 2915
Description: Weaker version of rexlimiv 2912. (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 2912 1  |-  ( E. x  e.  A  ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1869   E.wrex 2777
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749
This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1661  df-ral 2781  df-rex 2782
This theorem is referenced by:  r19.29vva  2973  sbcreu  3377  eliun  4302  reusv3i  4629  elrnmptg  5101  fvelrnb  5926  fvelimab  5935  iinpreima  6023  fmpt  6056  fliftfun  6218  elrnmpt2  6421  ovelrn  6457  onuninsuci  6679  fun11iun  6765  releldm2  6855  tfrlem4  7103  iiner  7441  elixpsn  7567  isfi  7598  card2on  8073  tz9.12lem1  8261  rankwflemb  8267  rankxpsuc  8356  scott0  8360  isnum2  8382  cardiun  8419  cardalephex  8523  dfac5lem4  8559  dfac12k  8579  cflim2  8695  cfss  8697  cfslb2n  8700  enfin2i  8753  fin23lem30  8774  itunitc  8853  axdc3lem2  8883  iundom2g  8967  pwcfsdom  9010  cfpwsdom  9011  tskr1om2  9195  genpelv  9427  prlem934  9460  suplem1pr  9479  supexpr  9481  supsrlem  9537  supsr  9538  fimaxre3  10555  iswrd  12670  iswrdOLD  12671  caurcvgr  13731  caurcvgrOLD  13732  caurcvg  13735  caurcvgOLD  13736  caucvg  13738  vdwapval  14916  restsspw  15323  mreunirn  15500  brssc  15712  arwhoma  15933  gexcl3  17232  dvdsr  17867  lspsnel  18219  lspprel  18310  ellspd  19352  iincld  20046  ssnei  20118  neindisj2  20131  neitr  20188  lecldbas  20227  tgcnp  20261  cncnp2  20289  lmmo  20388  is2ndc  20453  fbfinnfr  20848  fbunfip  20876  filunirn  20889  fbflim2  20984  flimcls  20992  hauspwpwf1  20994  flftg  21003  isfcls  21016  fclsbas  21028  isfcf  21041  ustfilxp  21219  ustbas  21234  restutop  21244  ucnima  21288  xmetunirn  21344  metss  21515  metrest  21531  restmetu  21577  qdensere  21782  elpi1  22068  lmmbr  22220  caun0  22243  nulmbl2  22482  itg2l  22679  aannenlem2  23277  taylfval  23306  ulmcl  23328  ulmpm  23330  ulmss  23344  tglnunirn  24585  ishpg  24793  3v3e3cycl1  25364  iseupa  25685  frgrancvvdeqlem4  25753  frg2wotn0  25776  usgreghash2spot  25789  hhcms  26848  hhsscms  26922  occllem  26948  occl  26949  chscllem2  27283  rabfmpunirn  28248  rhmdvdsr  28583  kerunit  28588  tpr2rico  28720  gsumesum  28882  esumcst  28886  esumfsup  28893  esumpcvgval  28901  esumcvg  28909  sigaclcuni  28942  mbfmfun  29078  dya2icoseg2  29102  bnj66  29673  bnj517  29698  rellyscon  29976  cvmliftlem15  30023  orderseqlem  30491  nofun  30537  norn  30539  dfrdg4  30717  brcolinear2  30824  brcolinear  30825  ellines  30918  poimirlem29  31889  volsupnfl  31905  unirep  31959  filbcmb  31987  islshpkrN  32611  ispointN  33232  pmapglbx  33259  rngunsnply  35965  usgra2pth  38972
  Copyright terms: Public domain W3C validator