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

Theorem rexlimivw 3011
Description: Weaker version of rexlimiv 3009. (Contributed by FL, 19-Sep-2011.)
Hypothesis
Ref Expression
rexlimivw.1 (𝜑𝜓)
Assertion
Ref Expression
rexlimivw (∃𝑥𝐴 𝜑𝜓)
Distinct variable group:   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥)

Proof of Theorem rexlimivw
StepHypRef Expression
1 rexlimivw.1 . . 3 (𝜑𝜓)
21a1i 11 . 2 (𝑥𝐴 → (𝜑𝜓))
32rexlimiv 3009 1 (∃𝑥𝐴 𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1977  wrex 2897
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827
This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-ral 2901  df-rex 2902
This theorem is referenced by:  r19.29vva  3062  r19.36v  3066  r19.44v  3075  r19.45v  3076  sbcreu  3482  eliun  4455  reusv3i  4796  elrnmptg  5283  fvelrnb  6138  fvelimab  6148  iinpreima  6238  fmpt  6274  fliftfun  6440  elrnmpt2  6649  ovelrn  6686  onuninsuci  6910  fun11iun  6997  releldm2  7087  tfrlem4  7340  iiner  7684  elixpsn  7811  isfi  7843  card2on  8320  tz9.12lem1  8511  rankwflemb  8517  rankxpsuc  8606  scott0  8610  isnum2  8632  cardiun  8669  cardalephex  8774  dfac5lem4  8810  dfac12k  8830  cflim2  8946  cfss  8948  cfslb2n  8951  enfin2i  9004  fin23lem30  9025  itunitc  9104  axdc3lem2  9134  iundom2g  9219  pwcfsdom  9262  cfpwsdom  9263  tskr1om2  9447  genpelv  9679  prlem934  9712  suplem1pr  9731  supexpr  9733  supsrlem  9789  supsr  9790  fimaxre3  10822  iswrd  13111  caurcvgr  14201  caurcvg  14204  caucvg  14206  vdwapval  15464  restsspw  15864  mreunirn  16033  brssc  16246  arwhoma  16467  gexcl3  17774  dvdsr  18418  lspsnel  18773  lspprel  18864  ellspd  19908  iincld  20601  ssnei  20672  neindisj2  20685  neitr  20742  lecldbas  20781  tgcnp  20815  cncnp2  20843  lmmo  20942  is2ndc  21007  fbfinnfr  21403  fbunfip  21431  filunirn  21444  fbflim2  21539  flimcls  21547  hauspwpwf1  21549  flftg  21558  isfcls  21571  fclsbas  21583  isfcf  21596  ustfilxp  21774  ustbas  21789  restutop  21799  ucnima  21843  xmetunirn  21900  metss  22071  metrest  22087  restmetu  22133  qdensere  22331  elpi1  22601  lmmbr  22809  caun0  22832  nulmbl2  23056  itg2l  23247  aannenlem2  23833  taylfval  23862  ulmcl  23884  ulmpm  23886  ulmss  23900  tglnunirn  25189  ishpg  25397  3v3e3cycl1  25966  iseupa  26286  frgrancvvdeqlem4  26354  frg2wotn0  26377  usgreghash2spot  26390  numclwwlkun  26400  hhcms  27238  hhsscms  27314  occllem  27340  occl  27341  chscllem2  27675  rabfmpunirn  28627  rhmdvdsr  28943  kerunit  28948  tpr2rico  29080  gsumesum  29242  esumcst  29246  esumfsup  29253  esumpcvgval  29261  esumcvg  29269  sigaclcuni  29302  mbfmfun  29437  dya2icoseg2  29461  bnj66  29978  bnj517  30003  rellyscon  30281  cvmliftlem15  30328  orderseqlem  30787  nofun  30840  norn  30842  dfrdg4  31022  brcolinear2  31129  brcolinear  31130  ellines  31223  poimirlem29  32402  volsupnfl  32418  unirep  32471  filbcmb  32499  islshpkrN  33219  ispointN  33840  pmapglbx  33867  rngunsnply  36556  uhgr1wlkspthlem1  40951  usgr2pth  40962  umgr2wlk  41148  frgrncvvdeqlem4  41464  frgr2wwlkn0  41485  fusgreg2wsp  41492  fusgreghash2wsp  41494  av-frgrareg  41540
  Copyright terms: Public domain W3C validator