Theorem rexlimivw 3130

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

Syntax hints:   → wi 4   ∈ wcel 2109  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3054

This theorem is referenced by:  r19.36v  3161  r19.45v  3169  r19.44v  3170  sbcreu  3836  eliun  4955  reusv3i  5354  elrnmptg  5914  fvelrnb  6903  fvelimab  6915  iinpreima  7023  fmpt  7064  fliftfun  7269  elrnmpo  7505  ovelrn  7545  onuninsuci  7796  fiunlem  7900  releldm2  8001  poxp2  8099  poxp3  8106  orderseqlem  8113  tfrlem4  8324  naddunif  8634  iiner  8739  elixpsn  8887  isfi  8924  card2on  9483  brttrcl  9642  tz9.12lem1  9716  rankwflemb  9722  rankxpsuc  9811  scott0  9815  isnum2  9874  cardiun  9911  cardalephex  10019  dfac5lem4  10055  dfac5lem4OLD  10057  dfac12k  10077  cflim2  10192  cfss  10194  cfslb2n  10197  enfin2i  10250  fin23lem30  10271  itunitc  10350  axdc3lem2  10380  iundom2g  10469  pwcfsdom  10512  cfpwsdom  10513  tskr1om2  10697  genpelv  10929  prlem934  10962  suplem1pr  10981  supexpr  10983  supsrlem  11040  supsr  11041  fimaxre3  12105  iswrd  14456  caurcvgr  15616  caurcvg  15619  caucvg  15621  vdwapval  16920  restsspw  17370  mreunirn  17538  brssc  17756  arwhoma  17987  gexcl3  19501  dvdsr  20282  rhmdvdsr  20428  ellspsn  20941  lspprel  21033  ellspd  21744  iincld  22959  ssnei  23030  neindisj2  23043  neitr  23100  lecldbas  23139  tgcnp  23173  cncnp2  23201  lmmo  23300  is2ndc  23366  fbfinnfr  23761  fbunfip  23789  filunirn  23802  fbflim2  23897  flimcls  23905  hauspwpwf1  23907  flftg  23916  isfcls  23929  fclsbas  23941  isfcf  23954  ustfilxp  24133  ustbas  24148  restutop  24158  ucnima  24201  xmetunirn  24258  metss  24429  metrest  24445  restmetu  24491  qdensere  24690  elpi1  24978  lmmbr  25191  caun0  25214  nulmbl2  25470  itg2l  25663  aannenlem2  26270  taylfval  26299  ulmcl  26323  ulmpm  26325  ulmss  26339  elno  27590  nofun  27594  norn  27596  madeval2  27798  elmade  27816  tglnunirn  28528  ishpg  28739  edglnl  29123  uhgrwkspthlem1  29733  usgr2pth  29744  umgr2wlk  29929  elwwlks2ons3  29935  clwwlknun  30091  frgrncvvdeqlem3  30280  frgr2wwlkn0  30307  frgrreg  30373  hhcms  31182  hhsscms  31257  occllem  31282  occl  31283  chscllem2  31617  r19.29ffa  32450  rabfmpunirn  32627  kerunit  33290  tpr2rico  33895  gsumesum  34042  esumcst  34046  esumfsup  34053  esumpcvgval  34061  esumcvg  34069  sigaclcuni  34101  mbfmfun  34236  dya2icoseg2  34262  bnj66  34843  bnj517  34868  cusgr3cyclex  35116  rellysconn  35231  cvmliftlem15  35278  satffunlem2lem1  35384  r1peuqusdeg1  35623  dfrdg4  35932  brcolinear2  36039  brcolinear  36040  ellines  36133  poimirlem29  37636  volsupnfl  37652  unirep  37701  filbcmb  37727  islshpkrN  39106  ispointN  39729  pmapglbx  39756  rngunsnply  43151  elsetpreimafvbi  47385  cycldlenngric  47921  grtrif1o  47934