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

Theorem rexlimivw 2943
Description: Weaker version of rexlimiv 2940. (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 2940 1  |-  ( E. x  e.  A  ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1823   E.wrex 2805
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1618  df-ral 2809  df-rex 2810
This theorem is referenced by:  r19.29vva  2998  sbcreu  3401  eliun  4320  reusv3i  4644  reusv7OLD  4649  elrnmptg  5241  fvelrnb  5895  fvelimab  5904  iinpreima  5993  fmpt  6028  fliftfun  6185  elrnmpt2  6388  ovelrn  6424  onuninsuci  6648  fun11iun  6733  releldm2  6823  tfrlem4  7040  iiner  7375  elixpsn  7501  isfi  7532  card2on  7972  tz9.12lem1  8196  rankwflemb  8202  rankxpsuc  8291  scott0  8295  isnum2  8317  cardiun  8354  cardalephex  8462  dfac5lem4  8498  dfac12k  8518  cflim2  8634  cfss  8636  cfslb2n  8639  enfin2i  8692  fin23lem30  8713  itunitc  8792  axdc3lem2  8822  iundom2g  8906  pwcfsdom  8949  cfpwsdom  8950  tskr1om2  9135  genpelv  9367  prlem934  9400  suplem1pr  9419  supexpr  9421  supsrlem  9477  supsr  9478  fimaxre3  10487  iswrd  12534  iswrdOLD  12535  caurcvgr  13578  caurcvg  13581  caucvg  13583  vdwapval  14575  restsspw  14921  mreunirn  15090  brssc  15302  arwhoma  15523  gexcl3  16806  dvdsr  17490  lspsnel  17844  lspprel  17935  ellspd  19004  iincld  19707  ssnei  19778  neindisj2  19791  neitr  19848  lecldbas  19887  tgcnp  19921  cncnp2  19949  lmmo  20048  is2ndc  20113  fbfinnfr  20508  fbunfip  20536  filunirn  20549  fbflim2  20644  flimcls  20652  hauspwpwf1  20654  flftg  20663  isfcls  20676  fclsbas  20688  isfcf  20701  ustfilxp  20881  ustbas  20896  restutop  20906  ucnima  20950  xmetunirn  21006  metss  21177  metrest  21193  restmetu  21256  qdensere  21443  elpi1  21711  lmmbr  21863  caun0  21886  nulmbl2  22113  itg2l  22302  aannenlem2  22891  taylfval  22920  ulmcl  22942  ulmpm  22944  ulmss  22958  tglnunirn  24136  ishpg  24329  3v3e3cycl1  24846  iseupa  25167  frgrancvvdeqlem4  25235  frg2wotn0  25258  usgreghash2spot  25271  hhcms  26318  hhsscms  26393  occllem  26419  occl  26420  chscllem2  26754  rabfmpunirn  27712  rhmdvdsr  28043  kerunit  28048  tpr2rico  28129  gsumesum  28288  esumcst  28292  esumfsup  28299  esumpcvgval  28307  esumcvg  28315  sigaclcuni  28348  mbfmfun  28462  dya2icoseg2  28486  rellyscon  28960  cvmliftlem15  29007  orderseqlem  29572  nofun  29649  norn  29651  dfrdg4  29828  brcolinear2  29936  brcolinear  29937  ellines  30030  volsupnfl  30299  unirep  30443  filbcmb  30471  rngunsnply  31363  usgra2pth  32726  bnj66  34319  bnj517  34344  islshpkrN  35242  ispointN  35863  pmapglbx  35890
  Copyright terms: Public domain W3C validator