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

Theorem rexlimivw 3058
Description: Weaker version of rexlimiv 3056. (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 3056 1 (∃𝑥𝐴 𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  wrex 2942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-ral 2946  df-rex 2947
This theorem is referenced by:  r19.29vva  3110  r19.36v  3114  r19.44v  3123  r19.45v  3124  sbcreu  3548  eliun  4556  reusv3i  4905  elrnmptg  5407  fvelrnb  6282  fvelimab  6292  iinpreima  6385  fmpt  6421  fliftfun  6602  elrnmpt2  6815  ovelrn  6852  onuninsuci  7082  fun11iun  7168  releldm2  7262  tfrlem4  7520  iiner  7862  elixpsn  7989  isfi  8021  card2on  8500  tz9.12lem1  8688  rankwflemb  8694  rankxpsuc  8783  scott0  8787  isnum2  8809  cardiun  8846  cardalephex  8951  dfac5lem4  8987  dfac12k  9007  cflim2  9123  cfss  9125  cfslb2n  9128  enfin2i  9181  fin23lem30  9202  itunitc  9281  axdc3lem2  9311  iundom2g  9400  pwcfsdom  9443  cfpwsdom  9444  tskr1om2  9628  genpelv  9860  prlem934  9893  suplem1pr  9912  supexpr  9914  supsrlem  9970  supsr  9971  fimaxre3  11008  iswrd  13339  caurcvgr  14448  caurcvg  14451  caucvg  14453  vdwapval  15724  restsspw  16139  mreunirn  16308  brssc  16521  arwhoma  16742  gexcl3  18048  dvdsr  18692  lspsnel  19051  lspprel  19142  ellspd  20189  iincld  20891  ssnei  20962  neindisj2  20975  neitr  21032  lecldbas  21071  tgcnp  21105  cncnp2  21133  lmmo  21232  is2ndc  21297  fbfinnfr  21692  fbunfip  21720  filunirn  21733  fbflim2  21828  flimcls  21836  hauspwpwf1  21838  flftg  21847  isfcls  21860  fclsbas  21872  isfcf  21885  ustfilxp  22063  ustbas  22078  restutop  22088  ucnima  22132  xmetunirn  22189  metss  22360  metrest  22376  restmetu  22422  qdensere  22620  elpi1  22891  lmmbr  23102  caun0  23125  nulmbl2  23350  itg2l  23541  aannenlem2  24129  taylfval  24158  ulmcl  24180  ulmpm  24182  ulmss  24196  tglnunirn  25488  ishpg  25696  edglnl  26083  uhgrwkspthlem1  26705  usgr2pth  26716  umgr2wlk  26914  elwwlks2ons3  26920  clwwlknun  27087  frgrncvvdeqlem3  27281  frgr2wwlkn0  27308  frgrreg  27381  hhcms  28188  hhsscms  28264  occllem  28290  occl  28291  chscllem2  28625  r19.29ffa  29448  rabfmpunirn  29581  rhmdvdsr  29946  kerunit  29951  tpr2rico  30086  gsumesum  30249  esumcst  30253  esumfsup  30260  esumpcvgval  30268  esumcvg  30276  sigaclcuni  30309  mbfmfun  30444  dya2icoseg2  30468  bnj66  31056  bnj517  31081  rellysconn  31359  cvmliftlem15  31406  orderseqlem  31877  nofun  31927  norn  31929  madeval2  32061  dfrdg4  32183  brcolinear2  32290  brcolinear  32291  ellines  32384  poimirlem29  33568  volsupnfl  33584  unirep  33637  filbcmb  33665  islshpkrN  34725  ispointN  35346  pmapglbx  35373  rngunsnply  38060
  Copyright terms: Public domain W3C validator