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  4460  reusv3i  4801  elrnmptg  5296  fvelrnb  6153  fvelimab  6163  iinpreima  6253  fmpt  6289  fliftfun  6462  elrnmpt2  6671  ovelrn  6708  onuninsuci  6932  fun11iun  7019  releldm2  7109  tfrlem4  7362  iiner  7706  elixpsn  7833  isfi  7865  card2on  8342  tz9.12lem1  8533  rankwflemb  8539  rankxpsuc  8628  scott0  8632  isnum2  8654  cardiun  8691  cardalephex  8796  dfac5lem4  8832  dfac12k  8852  cflim2  8968  cfss  8970  cfslb2n  8973  enfin2i  9026  fin23lem30  9047  itunitc  9126  axdc3lem2  9156  iundom2g  9241  pwcfsdom  9284  cfpwsdom  9285  tskr1om2  9469  genpelv  9701  prlem934  9734  suplem1pr  9753  supexpr  9755  supsrlem  9811  supsr  9812  fimaxre3  10849  iswrd  13162  caurcvgr  14252  caurcvg  14255  caucvg  14257  vdwapval  15515  restsspw  15915  mreunirn  16084  brssc  16297  arwhoma  16518  gexcl3  17825  dvdsr  18469  lspsnel  18824  lspprel  18915  ellspd  19960  iincld  20653  ssnei  20724  neindisj2  20737  neitr  20794  lecldbas  20833  tgcnp  20867  cncnp2  20895  lmmo  20994  is2ndc  21059  fbfinnfr  21455  fbunfip  21483  filunirn  21496  fbflim2  21591  flimcls  21599  hauspwpwf1  21601  flftg  21610  isfcls  21623  fclsbas  21635  isfcf  21648  ustfilxp  21826  ustbas  21841  restutop  21851  ucnima  21895  xmetunirn  21952  metss  22123  metrest  22139  restmetu  22185  qdensere  22383  elpi1  22653  lmmbr  22864  caun0  22887  nulmbl2  23111  itg2l  23302  aannenlem2  23888  taylfval  23917  ulmcl  23939  ulmpm  23941  ulmss  23955  tglnunirn  25243  ishpg  25451  3v3e3cycl1  26172  iseupa  26492  frgrancvvdeqlem4  26560  frg2wotn0  26583  usgreghash2spot  26596  numclwwlkun  26606  hhcms  27444  hhsscms  27520  occllem  27546  occl  27547  chscllem2  27881  rabfmpunirn  28833  rhmdvdsr  29149  kerunit  29154  tpr2rico  29286  gsumesum  29448  esumcst  29452  esumfsup  29459  esumpcvgval  29467  esumcvg  29475  sigaclcuni  29508  mbfmfun  29643  dya2icoseg2  29667  bnj66  30184  bnj517  30209  rellyscon  30487  cvmliftlem15  30534  orderseqlem  30993  nofun  31046  norn  31048  dfrdg4  31228  brcolinear2  31335  brcolinear  31336  ellines  31429  poimirlem29  32608  volsupnfl  32624  unirep  32677  filbcmb  32705  islshpkrN  33425  ispointN  34046  pmapglbx  34073  rngunsnply  36762  uhgr1wlkspthlem1  40959  usgr2pth  40970  umgr2wlk  41156  frgrncvvdeqlem4  41472  frgr2wwlkn0  41493  fusgreg2wsp  41500  fusgreghash2wsp  41502  av-frgrareg  41548
  Copyright terms: Public domain W3C validator