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

Theorem rexlimivw 2876
Description: Weaker version of rexlimiv 2873. (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 2873 1  |-  ( E. x  e.  A  ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1887   E.wrex 2738
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758
This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1664  df-ral 2742  df-rex 2743
This theorem is referenced by:  r19.29vva  2934  sbcreu  3344  eliun  4283  reusv3i  4610  elrnmptg  5084  fvelrnb  5912  fvelimab  5921  iinpreima  6010  fmpt  6043  fliftfun  6205  elrnmpt2  6409  ovelrn  6445  onuninsuci  6667  fun11iun  6753  releldm2  6843  tfrlem4  7097  iiner  7435  elixpsn  7561  isfi  7593  card2on  8069  tz9.12lem1  8258  rankwflemb  8264  rankxpsuc  8353  scott0  8357  isnum2  8379  cardiun  8416  cardalephex  8521  dfac5lem4  8557  dfac12k  8577  cflim2  8693  cfss  8695  cfslb2n  8698  enfin2i  8751  fin23lem30  8772  itunitc  8851  axdc3lem2  8881  iundom2g  8965  pwcfsdom  9008  cfpwsdom  9009  tskr1om2  9193  genpelv  9425  prlem934  9458  suplem1pr  9477  supexpr  9479  supsrlem  9535  supsr  9536  fimaxre3  10553  iswrd  12672  iswrdOLD  12673  caurcvgr  13738  caurcvgrOLD  13739  caurcvg  13742  caurcvgOLD  13743  caucvg  13745  vdwapval  14923  restsspw  15330  mreunirn  15507  brssc  15719  arwhoma  15940  gexcl3  17239  dvdsr  17874  lspsnel  18226  lspprel  18317  ellspd  19360  iincld  20054  ssnei  20126  neindisj2  20139  neitr  20196  lecldbas  20235  tgcnp  20269  cncnp2  20297  lmmo  20396  is2ndc  20461  fbfinnfr  20856  fbunfip  20884  filunirn  20897  fbflim2  20992  flimcls  21000  hauspwpwf1  21002  flftg  21011  isfcls  21024  fclsbas  21036  isfcf  21049  ustfilxp  21227  ustbas  21242  restutop  21252  ucnima  21296  xmetunirn  21352  metss  21523  metrest  21539  restmetu  21585  qdensere  21790  elpi1  22076  lmmbr  22228  caun0  22251  nulmbl2  22490  itg2l  22687  aannenlem2  23285  taylfval  23314  ulmcl  23336  ulmpm  23338  ulmss  23352  tglnunirn  24593  ishpg  24801  3v3e3cycl1  25372  iseupa  25693  frgrancvvdeqlem4  25761  frg2wotn0  25784  usgreghash2spot  25797  hhcms  26856  hhsscms  26930  occllem  26956  occl  26957  chscllem2  27291  rabfmpunirn  28252  rhmdvdsr  28581  kerunit  28586  tpr2rico  28718  gsumesum  28880  esumcst  28884  esumfsup  28891  esumpcvgval  28899  esumcvg  28907  sigaclcuni  28940  mbfmfun  29076  dya2icoseg2  29100  bnj66  29671  bnj517  29696  rellyscon  29974  cvmliftlem15  30021  orderseqlem  30490  nofun  30536  norn  30538  dfrdg4  30718  brcolinear2  30825  brcolinear  30826  ellines  30919  poimirlem29  31969  volsupnfl  31985  unirep  32039  filbcmb  32067  islshpkrN  32686  ispointN  33307  pmapglbx  33334  rngunsnply  36039  usgra2pth  39721
  Copyright terms: Public domain W3C validator