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

Theorem rexlimivw 2827
Description: Weaker version of rexlimiv 2825. (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 2825 1  |-  ( E. x  e.  A  ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1755   E.wrex 2706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-12 1791
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-ral 2710  df-rex 2711
This theorem is referenced by:  r19.29_2a  2854  sbcreu  3261  eliun  4163  reusv3i  4487  reusv7OLD  4492  elrnmptg  5076  fvelrnb  5727  fvelimab  5735  iinpreima  5821  fmpt  5852  fliftfun  5992  elrnmpt2  6192  ovelrn  6228  onuninsuci  6440  fun11iun  6526  releldm2  6613  tfrlem4  6824  abianfp  6900  iiner  7160  elixpsn  7290  isfi  7321  card2on  7757  tz9.12lem1  7982  rankwflemb  7988  rankxpsuc  8077  scott0  8081  isnum2  8103  cardiun  8140  cardalephex  8248  dfac5lem4  8284  dfac12k  8304  cflim2  8420  cfss  8422  cfslb2n  8425  enfin2i  8478  fin23lem30  8499  itunitc  8578  axdc3lem2  8608  iundom2g  8692  pwcfsdom  8735  cfpwsdom  8736  tskr1om2  8923  gruiun  8954  genpelv  9157  prlem934  9190  suplem1pr  9209  supexpr  9211  supsrlem  9266  supsr  9267  fimaxre3  10267  iswrd  12221  caurcvgr  13135  caurcvg  13138  caucvg  13140  vdwapval  14017  restsspw  14353  mreunirn  14522  brssc  14710  arwhoma  14896  gexcl3  16066  dvdsr  16672  lspsnel  17006  lspprel  17097  ellspd  18072  ellspdOLD  18073  iincld  18485  ssnei  18556  neindisj2  18569  neitr  18626  lecldbas  18665  tgcnp  18699  cncnp2  18727  lmmo  18826  is2ndc  18892  fbfinnfr  19256  fbunfip  19284  filunirn  19297  fbflim2  19392  flimcls  19400  hauspwpwf1  19402  flftg  19411  isfcls  19424  fclsbas  19436  isfcf  19449  ustfilxp  19629  ustbas  19644  restutop  19654  ucnima  19698  xmetunirn  19754  metss  19925  metrest  19941  restmetu  20004  qdensere  20191  elpi1  20459  lmmbr  20611  caun0  20634  nulmbl2  20860  itg2l  21049  aannenlem2  21680  taylfval  21709  ulmcl  21731  ulmpm  21733  ulmss  21747  tglnunirn  22863  3v3e3cycl1  23353  iseupa  23409  hhcms  24428  hhsscms  24503  occllem  24529  occl  24530  chscllem2  24864  rabfmpunirn  25792  rhmdvdsr  26139  kerunit  26144  tpr2rico  26196  gsumesum  26364  esumcst  26368  esumfsup  26373  esumpcvgval  26381  esumcvg  26389  sigaclcuni  26415  mbfmfun  26523  dya2icoseg2  26547  rellyscon  26988  cvmliftlem15  27035  orderseqlem  27560  nofun  27637  norn  27639  dfrdg4  27828  brcolinear2  27936  brcolinear  27937  ellines  28030  volsupnfl  28280  unirep  28450  filbcmb  28478  rngunsnply  29375  usgra2pth  30147  frgrancvvdeqlem4  30472  frg2wotn0  30495  usgreghash2spot  30508  bnj66  31555  bnj517  31580  islshpkrN  32338  ispointN  32959  pmapglbx  32986
  Copyright terms: Public domain W3C validator