Theorem rexlimivw 3151

Description: Weaker version of rexlimiv 3148. (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 482	. 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓)
3	2	rexlimiva 3147	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2106  ∃wrex 3070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-rex 3071

This theorem is referenced by:  r19.36v  3183  r19.45v  3192  r19.44v  3193  r19.29vvaOLD  3214  sbcreu  3870  eliun  5001  reusv3i  5402  elrnmptg  5958  fvelrnb  6952  fvelimab  6964  iinpreima  7070  fmpt  7111  fliftfun  7311  elrnmpo  7547  ovelrn  7585  onuninsuci  7831  fiunlem  7930  releldm2  8031  poxp2  8131  poxp3  8138  orderseqlem  8145  tfrlem4  8381  naddunif  8694  iiner  8785  elixpsn  8933  isfi  8974  card2on  9551  brttrcl  9710  tz9.12lem1  9784  rankwflemb  9790  rankxpsuc  9879  scott0  9883  isnum2  9942  cardiun  9979  cardalephex  10087  dfac5lem4  10123  dfac12k  10144  cflim2  10260  cfss  10262  cfslb2n  10265  enfin2i  10318  fin23lem30  10339  itunitc  10418  axdc3lem2  10448  iundom2g  10537  pwcfsdom  10580  cfpwsdom  10581  tskr1om2  10765  genpelv  10997  prlem934  11030  suplem1pr  11049  supexpr  11051  supsrlem  11108  supsr  11109  fimaxre3  12162  iswrd  14468  caurcvgr  15622  caurcvg  15625  caucvg  15627  vdwapval  16908  restsspw  17379  mreunirn  17547  brssc  17763  arwhoma  17997  gexcl3  19457  dvdsr  20180  rhmdvdsr  20291  lspsnel  20619  lspprel  20710  ellspd  21363  iincld  22550  ssnei  22621  neindisj2  22634  neitr  22691  lecldbas  22730  tgcnp  22764  cncnp2  22792  lmmo  22891  is2ndc  22957  fbfinnfr  23352  fbunfip  23380  filunirn  23393  fbflim2  23488  flimcls  23496  hauspwpwf1  23498  flftg  23507  isfcls  23520  fclsbas  23532  isfcf  23545  ustfilxp  23724  ustbas  23739  restutop  23749  ucnima  23793  xmetunirn  23850  metss  24024  metrest  24040  restmetu  24086  qdensere  24293  elpi1  24568  lmmbr  24782  caun0  24805  nulmbl2  25060  itg2l  25254  aannenlem2  25849  taylfval  25878  ulmcl  25900  ulmpm  25902  ulmss  25916  nofun  27159  norn  27161  madeval2  27356  elmade  27370  tglnunirn  27837  ishpg  28048  edglnl  28441  uhgrwkspthlem1  29048  usgr2pth  29059  umgr2wlk  29241  elwwlks2ons3  29247  clwwlknun  29403  frgrncvvdeqlem3  29592  frgr2wwlkn0  29619  frgrreg  29685  hhcms  30494  hhsscms  30569  occllem  30594  occl  30595  chscllem2  30929  r19.29ffa  31751  rabfmpunirn  31916  kerunit  32478  tpr2rico  32961  gsumesum  33126  esumcst  33130  esumfsup  33137  esumpcvgval  33145  esumcvg  33153  sigaclcuni  33185  mbfmfun  33320  dya2icoseg2  33346  bnj66  33940  bnj517  33965  cusgr3cyclex  34196  rellysconn  34311  cvmliftlem15  34358  satffunlem2lem1  34464  dfrdg4  34992  brcolinear2  35099  brcolinear  35100  ellines  35193  poimirlem29  36603  volsupnfl  36619  unirep  36668  filbcmb  36694  islshpkrN  38076  ispointN  38699  pmapglbx  38726  rngunsnply  41997  elsetpreimafvbi  46138