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

Theorem rexlimivw 3217
Description: Weaker version of rexlimiv 3215. (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 3215 1 (∃𝑥𝐴 𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2156  wrex 3097
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-ral 3101  df-rex 3102
This theorem is referenced by:  r19.29vva  3269  r19.36v  3273  r19.44v  3282  r19.45v  3283  sbcreu  3710  eliun  4716  reusv3i  5073  elrnmptg  5576  fvelrnb  6464  fvelimab  6474  iinpreima  6567  fmpt  6602  fliftfun  6786  elrnmpt2  7003  ovelrn  7040  onuninsuci  7270  fun11iun  7356  releldm2  7450  tfrlem4  7711  iiner  8054  elixpsn  8184  isfi  8216  card2on  8698  tz9.12lem1  8897  rankwflemb  8903  rankxpsuc  8992  scott0  8996  isnum2  9054  cardiun  9091  cardalephex  9196  dfac5lem4  9232  dfac12k  9254  cflim2  9370  cfss  9372  cfslb2n  9375  enfin2i  9428  fin23lem30  9449  itunitc  9528  axdc3lem2  9558  iundom2g  9647  pwcfsdom  9690  cfpwsdom  9691  tskr1om2  9875  genpelv  10107  prlem934  10140  suplem1pr  10159  supexpr  10161  supsrlem  10217  supsr  10218  fimaxre3  11255  iswrd  13518  caurcvgr  14627  caurcvg  14630  caucvg  14632  vdwapval  15894  restsspw  16297  mreunirn  16466  brssc  16678  arwhoma  16899  gexcl3  18203  dvdsr  18848  lspsnel  19210  lspprel  19301  ellspd  20351  iincld  21057  ssnei  21128  neindisj2  21141  neitr  21198  lecldbas  21237  tgcnp  21271  cncnp2  21299  lmmo  21398  is2ndc  21463  fbfinnfr  21858  fbunfip  21886  filunirn  21899  fbflim2  21994  flimcls  22002  hauspwpwf1  22004  flftg  22013  isfcls  22026  fclsbas  22038  isfcf  22051  ustfilxp  22229  ustbas  22244  restutop  22254  ucnima  22298  xmetunirn  22355  metss  22526  metrest  22542  restmetu  22588  qdensere  22786  elpi1  23057  lmmbr  23268  caun0  23291  nulmbl2  23517  itg2l  23710  aannenlem2  24298  taylfval  24327  ulmcl  24349  ulmpm  24351  ulmss  24365  tglnunirn  25657  ishpg  25865  edglnl  26253  uhgrwkspthlem1  26877  usgr2pth  26888  umgr2wlk  27089  elwwlks2ons3  27095  clwwlknun  27281  frgrncvvdeqlem3  27476  frgr2wwlkn0  27503  frgrreg  27582  hhcms  28388  hhsscms  28464  occllem  28490  occl  28491  chscllem2  28825  r19.29ffa  29648  rabfmpunirn  29780  rhmdvdsr  30143  kerunit  30148  tpr2rico  30283  gsumesum  30446  esumcst  30450  esumfsup  30457  esumpcvgval  30465  esumcvg  30473  sigaclcuni  30506  mbfmfun  30641  dya2icoseg2  30665  bnj66  31253  bnj517  31278  rellysconn  31556  cvmliftlem15  31603  orderseqlem  32073  nofun  32123  norn  32125  madeval2  32257  dfrdg4  32379  brcolinear2  32486  brcolinear  32487  ellines  32580  poimirlem29  33751  volsupnfl  33767  unirep  33819  filbcmb  33847  islshpkrN  34900  ispointN  35522  pmapglbx  35549  rngunsnply  38244
  Copyright terms: Public domain W3C validator