Theorem rexlimivw 3152

Description: Weaker version of rexlimiv 3149. (Contributed by FL, 19-Sep-2011.) (Proof shortened by Wolf Lammen, 23-Dec-2024.)

Hypothesis

Ref	Expression
rexlimivw.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
rexlimivw	⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

Distinct variable group:   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥)

Proof of Theorem rexlimivw

Step	Hyp	Ref	Expression
1		rexlimivw.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	adantl 483	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓)
3	2	rexlimiva 3148	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2107  ∃wrex 3071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-rex 3072

This theorem is referenced by:  r19.36v  3184  r19.45v  3193  r19.44v  3194  r19.29vvaOLD  3215  sbcreu  3869  eliun  5000  reusv3i  5401  elrnmptg  5956  fvelrnb  6949  fvelimab  6960  iinpreima  7066  fmpt  7105  fliftfun  7304  elrnmpo  7540  ovelrn  7578  onuninsuci  7824  fiunlem  7923  releldm2  8024  poxp2  8124  poxp3  8131  orderseqlem  8138  tfrlem4  8374  naddunif  8688  iiner  8779  elixpsn  8927  isfi  8968  card2on  9545  brttrcl  9704  tz9.12lem1  9778  rankwflemb  9784  rankxpsuc  9873  scott0  9877  isnum2  9936  cardiun  9973  cardalephex  10081  dfac5lem4  10117  dfac12k  10138  cflim2  10254  cfss  10256  cfslb2n  10259  enfin2i  10312  fin23lem30  10333  itunitc  10412  axdc3lem2  10442  iundom2g  10531  pwcfsdom  10574  cfpwsdom  10575  tskr1om2  10759  genpelv  10991  prlem934  11024  suplem1pr  11043  supexpr  11045  supsrlem  11102  supsr  11103  fimaxre3  12156  iswrd  14462  caurcvgr  15616  caurcvg  15619  caucvg  15621  vdwapval  16902  restsspw  17373  mreunirn  17541  brssc  17757  arwhoma  17991  gexcl3  19448  dvdsr  20165  rhmdvdsr  20276  lspsnel  20602  lspprel  20693  ellspd  21341  iincld  22525  ssnei  22596  neindisj2  22609  neitr  22666  lecldbas  22705  tgcnp  22739  cncnp2  22767  lmmo  22866  is2ndc  22932  fbfinnfr  23327  fbunfip  23355  filunirn  23368  fbflim2  23463  flimcls  23471  hauspwpwf1  23473  flftg  23482  isfcls  23495  fclsbas  23507  isfcf  23520  ustfilxp  23699  ustbas  23714  restutop  23724  ucnima  23768  xmetunirn  23825  metss  23999  metrest  24015  restmetu  24061  qdensere  24268  elpi1  24543  lmmbr  24757  caun0  24780  nulmbl2  25035  itg2l  25229  aannenlem2  25824  taylfval  25853  ulmcl  25875  ulmpm  25877  ulmss  25891  nofun  27132  norn  27134  madeval2  27328  elmade  27342  tglnunirn  27779  ishpg  27990  edglnl  28383  uhgrwkspthlem1  28990  usgr2pth  29001  umgr2wlk  29183  elwwlks2ons3  29189  clwwlknun  29345  frgrncvvdeqlem3  29534  frgr2wwlkn0  29561  frgrreg  29627  hhcms  30434  hhsscms  30509  occllem  30534  occl  30535  chscllem2  30869  r19.29ffa  31691  rabfmpunirn  31856  kerunit  32406  tpr2rico  32830  gsumesum  32995  esumcst  32999  esumfsup  33006  esumpcvgval  33014  esumcvg  33022  sigaclcuni  33054  mbfmfun  33189  dya2icoseg2  33215  bnj66  33809  bnj517  33834  cusgr3cyclex  34065  rellysconn  34180  cvmliftlem15  34227  satffunlem2lem1  34333  dfrdg4  34861  brcolinear2  34968  brcolinear  34969  ellines  35062  poimirlem29  36455  volsupnfl  36471  unirep  36520  filbcmb  36546  islshpkrN  37928  ispointN  38551  pmapglbx  38578  rngunsnply  41848  elsetpreimafvbi  45994