Theorem rexlimivw 3126

Description: Weaker version of rexlimiv 3123. (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 3122	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  3157  r19.45v  3163  r19.44v  3164  sbcreu  3828  eliun  4945  reusv3i  5343  elrnmptg  5903  fvelrnb  6883  fvelimab  6895  iinpreima  7003  fmpt  7044  fliftfun  7249  elrnmpo  7485  ovelrn  7525  onuninsuci  7773  fiunlem  7877  releldm2  7978  poxp2  8076  poxp3  8083  orderseqlem  8090  tfrlem4  8301  naddunif  8611  iiner  8716  elixpsn  8864  isfi  8901  card2on  9446  brttrcl  9609  tz9.12lem1  9683  rankwflemb  9689  rankxpsuc  9778  scott0  9782  isnum2  9841  cardiun  9878  cardalephex  9984  dfac5lem4  10020  dfac5lem4OLD  10022  dfac12k  10042  cflim2  10157  cfss  10159  cfslb2n  10162  enfin2i  10215  fin23lem30  10236  itunitc  10315  axdc3lem2  10345  iundom2g  10434  pwcfsdom  10477  cfpwsdom  10478  tskr1om2  10662  genpelv  10894  prlem934  10927  suplem1pr  10946  supexpr  10948  supsrlem  11005  supsr  11006  fimaxre3  12071  iswrd  14422  caurcvgr  15581  caurcvg  15584  caucvg  15586  vdwapval  16885  restsspw  17335  mreunirn  17503  brssc  17721  arwhoma  17952  gexcl3  19466  dvdsr  20247  rhmdvdsr  20393  ellspsn  20906  lspprel  20998  ellspd  21709  iincld  22924  ssnei  22995  neindisj2  23008  neitr  23065  lecldbas  23104  tgcnp  23138  cncnp2  23166  lmmo  23265  is2ndc  23331  fbfinnfr  23726  fbunfip  23754  filunirn  23767  fbflim2  23862  flimcls  23870  hauspwpwf1  23872  flftg  23881  isfcls  23894  fclsbas  23906  isfcf  23919  ustfilxp  24098  ustbas  24113  restutop  24123  ucnima  24166  xmetunirn  24223  metss  24394  metrest  24410  restmetu  24456  qdensere  24655  elpi1  24943  lmmbr  25156  caun0  25179  nulmbl2  25435  itg2l  25628  aannenlem2  26235  taylfval  26264  ulmcl  26288  ulmpm  26290  ulmss  26304  elno  27555  nofun  27559  norn  27561  madeval2  27763  elmade  27781  tglnunirn  28493  ishpg  28704  edglnl  29088  uhgrwkspthlem1  29698  usgr2pth  29709  umgr2wlk  29894  elwwlks2ons3  29900  clwwlknun  30056  frgrncvvdeqlem3  30245  frgr2wwlkn0  30272  frgrreg  30338  hhcms  31147  hhsscms  31222  occllem  31247  occl  31248  chscllem2  31582  r19.29ffa  32415  rabfmpunirn  32596  kerunit  33263  tpr2rico  33879  gsumesum  34026  esumcst  34030  esumfsup  34037  esumpcvgval  34045  esumcvg  34053  sigaclcuni  34085  mbfmfun  34220  dya2icoseg2  34246  bnj66  34827  bnj517  34852  cusgr3cyclex  35109  rellysconn  35224  cvmliftlem15  35271  satffunlem2lem1  35377  r1peuqusdeg1  35616  dfrdg4  35925  brcolinear2  36032  brcolinear  36033  ellines  36126  poimirlem29  37629  volsupnfl  37645  unirep  37694  filbcmb  37720  islshpkrN  39099  ispointN  39721  pmapglbx  39748  rngunsnply  43142  elsetpreimafvbi  47375  cycldlenngric  47912  grtrif1o  47926