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

Theorem rexlimivw 2786
Description: Weaker version of rexlimiv 2784. (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 2784 1  |-  ( E. x  e.  A  ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1721   E.wrex 2667
This theorem is referenced by:  r19.29_2a  2812  eliun  4057  reusv3i  4689  reusv7OLD  4694  onuninsuci  4779  elrnmptg  5079  fun11iun  5654  fvelrnb  5733  fvelimab  5741  iinpreima  5819  fmpt  5849  fliftfun  5993  elrnmpt2  6142  ovelrn  6181  releldm2  6356  tfrlem4  6599  abianfp  6675  iiner  6935  elixpsn  7060  isfi  7090  card2on  7478  tz9.12lem1  7669  rankwflemb  7675  rankxpsuc  7762  scott0  7766  isnum2  7788  cardiun  7825  cardalephex  7927  dfac5lem4  7963  dfac12k  7983  cflim2  8099  cfss  8101  cfslb2n  8104  enfin2i  8157  fin23lem30  8178  itunitc  8257  axdc3lem2  8287  iundom2g  8371  pwcfsdom  8414  cfpwsdom  8415  tskr1om2  8599  gruiun  8630  genpelv  8833  prlem934  8866  suplem1pr  8885  supexpr  8887  supsrlem  8942  supsr  8943  fimaxre3  9913  iswrd  11684  caurcvgr  12422  caurcvg  12425  caucvg  12427  vdwapval  13296  restsspw  13614  mreunirn  13781  brssc  13969  arwhoma  14155  gexcl3  15176  dvdsr  15706  lspsnel  16034  lspprel  16121  iincld  17058  ssnei  17129  neindisj2  17142  neitr  17198  lecldbas  17237  tgcnp  17271  cncnp2  17299  lmmo  17398  is2ndc  17462  fbfinnfr  17826  fbunfip  17854  filunirn  17867  fbflim2  17962  flimcls  17970  hauspwpwf1  17972  flftg  17981  isfcls  17994  fclsbas  18006  isfcf  18019  ustfilxp  18195  ustbas  18210  restutop  18220  ucnima  18264  xmetunirn  18320  metss  18491  metrest  18507  restmetu  18570  qdensere  18757  elpi1  19023  lmmbr  19164  caun0  19187  nulmbl2  19384  itg2l  19574  aannenlem2  20199  taylfval  20228  ulmcl  20250  ulmpm  20252  ulmss  20266  3v3e3cycl1  21584  iseupa  21640  hhcms  22658  hhsscms  22732  occllem  22758  occl  22759  chscllem2  23093  rabfmpunirn  24018  rhmdvdsr  24209  kerunit  24214  tpr2rico  24263  gsumesum  24404  esumcst  24408  esumfsup  24413  esumpcvgval  24421  esumcvg  24429  sigaclcuni  24454  mbfmfun  24557  dya2icoseg2  24581  rellyscon  24891  cvmliftlem15  24938  orderseqlem  25466  nofun  25517  norn  25519  dfrdg4  25703  brcolinear2  25896  brcolinear  25897  ellines  25990  volsupnfl  26150  unirep  26304  filbcmb  26332  ellspd  27122  rngunsnply  27246  usgra2pth  28041  frgrancvvdeqlem4  28136  frg2wotn0  28159  usgreghash2spot  28172  bnj66  28937  bnj517  28962  islshpkrN  29603  ispointN  30224  pmapglbx  30251
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-11 1757
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-ral 2671  df-rex 2672
  Copyright terms: Public domain W3C validator