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

Theorem rexlimivw 3286
Description: Weaker version of rexlimiv 3284. (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 3284 1 (∃𝑥𝐴 𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  wrex 3143
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-ral 3147  df-rex 3148
This theorem is referenced by:  r19.29vva  3340  r19.29vvaOLD  3341  r19.36v  3346  r19.44v  3356  r19.45v  3357  sbcreu  3862  eliun  4920  reusv3i  5300  elrnmptg  5829  fvelrnb  6722  fvelimab  6733  iinpreima  6832  fmpt  6869  fliftfun  7060  elrnmpo  7280  ovelrn  7317  onuninsuci  7546  fiunlemw  7634  fiunlem  7637  releldm2  7736  tfrlem4  8009  iiner  8362  elixpsn  8493  isfi  8525  card2on  9010  tz9.12lem1  9208  rankwflemb  9214  rankxpsuc  9303  scott0  9307  isnum2  9366  cardiun  9403  cardalephex  9508  dfac5lem4  9544  dfac12k  9565  cflim2  9677  cfss  9679  cfslb2n  9682  enfin2i  9735  fin23lem30  9756  itunitc  9835  axdc3lem2  9865  iundom2g  9954  pwcfsdom  9997  cfpwsdom  9998  tskr1om2  10182  genpelv  10414  prlem934  10447  suplem1pr  10466  supexpr  10468  supsrlem  10525  supsr  10526  fimaxre3  11579  iswrd  13856  caurcvgr  15023  caurcvg  15026  caucvg  15028  vdwapval  16301  restsspw  16697  mreunirn  16864  brssc  17076  arwhoma  17297  gexcl3  18634  dvdsr  19318  lspsnel  19697  lspprel  19788  ellspd  20862  iincld  21563  ssnei  21634  neindisj2  21647  neitr  21704  lecldbas  21743  tgcnp  21777  cncnp2  21805  lmmo  21904  is2ndc  21970  fbfinnfr  22365  fbunfip  22393  filunirn  22406  fbflim2  22501  flimcls  22509  hauspwpwf1  22511  flftg  22520  isfcls  22533  fclsbas  22545  isfcf  22558  ustfilxp  22736  ustbas  22751  restutop  22761  ucnima  22805  xmetunirn  22862  metss  23033  metrest  23049  restmetu  23095  qdensere  23293  elpi1  23564  lmmbr  23776  caun0  23799  nulmbl2  24052  itg2l  24245  aannenlem2  24833  taylfval  24862  ulmcl  24884  ulmpm  24886  ulmss  24900  tglnunirn  26248  ishpg  26459  edglnl  26842  uhgrwkspthlem1  27448  usgr2pth  27459  umgr2wlk  27642  elwwlks2ons3  27648  clwwlknun  27805  frgrncvvdeqlem3  27994  frgr2wwlkn0  28021  frgrreg  28087  hhcms  28894  hhsscms  28969  occllem  28994  occl  28995  chscllem2  29329  r19.29ffa  30151  rabfmpunirn  30313  rhmdvdsr  30805  kerunit  30810  tpr2rico  31041  gsumesum  31204  esumcst  31208  esumfsup  31215  esumpcvgval  31223  esumcvg  31231  sigaclcuni  31263  mbfmfun  31398  dya2icoseg2  31422  bnj66  32018  bnj517  32043  cusgr3cyclex  32267  rellysconn  32382  cvmliftlem15  32429  satffunlem2lem1  32535  orderseqlem  32978  nofun  33040  norn  33042  madeval2  33174  dfrdg4  33296  brcolinear2  33403  brcolinear  33404  ellines  33497  poimirlem29  34788  volsupnfl  34804  unirep  34856  filbcmb  34883  islshpkrN  36123  ispointN  36745  pmapglbx  36772  rngunsnply  39634
  Copyright terms: Public domain W3C validator