Theorem rexlimivw 3163

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ∃wrex 3090

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3091

This theorem is used by:  r19.36v  3194  r19.45v  3200  r19.44v  3201  sbcreu  3827  eliun  4960  reusv3i  5373  elrnmptg  5955  fvelrnb  6976  fvelimab  6988  iinpreima  7101  fmpt  7142  fliftfun  7351  elrnmpo  7588  ovelrn  7629  onuninsuci  7885  fiunlem  7988  releldm2  8088  poxp2  8197  poxp3  8204  orderseqlem  8211  tfrlem4  8424  naddunif  8741  iiner  8848  elixpsn  9003  isfi  9040  card2on  9585  brttrcl  9751  tz9.12lem1  9831  rankwflemb  9837  rankwflembOLD  9838  rankxpsuc  9936  scott0b  9974  scott0OLD  9975  isnum2  10063  cardiun  10102  cardalephex  10208  dfac5lem4  10244  dfac12k  10265  cflim2  10380  cfss  10382  cfslb2n  10385  enfin2i  10438  fin23lem30  10459  itunitc  10538  axdc3lem2  10568  iundom2g  10663  pwcfsdom  10707  cfpwsdom  10708  tskhf  10892  genpelv  11124  prlem934  11157  suplem1pr  11176  supexpr  11178  supsrlem  11235  supsr  11236  fimaxre3  12303  iswrd  14701  caurcvgr  15885  caurcvg  15888  caucvg  15890  vdwapval  17195  restsspw  17652  mreunirn  17821  brssc  18039  arwhoma  18270  gexcl3  19852  dvdsr  20643  rhmdvdsr  20809  ellspsn  21329  lspprel  21420  ellspd  22163  iincld  23412  ssnei  23483  neindisj2  23496  neitr  23553  lecldbas  23592  tgcnp  23626  cncnp2  23654  lmmo  23753  is2ndc  23819  fbfinnfr  24215  fbunfip  24243  filunirn  24256  fbflim2  24351  flimcls  24359  hauspwpwf1  24361  flftg  24370  isfcls  24383  fclsbas  24395  isfcf  24408  ustfilxp  24587  ustbas  24601  restutop  24611  ucnima  24654  xmetunirn  24711  metss  24882  metrest  24898  restmetu  24944  qdensere  25143  elpi1  25421  lmmbr  25634  caun0  25657  nulmbl2  25912  itg2l  26105  rngunsnply  26693  aannenlem2  26713  taylfval  26743  ulmcl  26765  ulmpm  26767  ulmss  26781  elno  28060  nofun  28063  norn  28065  madeval2  28276  elmade  28300  tglnunirn  29068  ishpg  29294  edglnl  29778  uhgrwkspthlem1  30396  usgr2pth  30407  umgr2wlk  30595  elwwlks2ons3  30601  clwwlknun  30760  frgrncvvdeqlem3  30959  frgr2wwlkn0  30986  frgrreg  31052  hhcms  31862  hhsscms  31937  occllem  31962  occl  31963  chscllem2  32297  r19.29ffa  33167  rabfmpunirn  33345  kerunit  33990  tpr2rico  34655  gsumesum  34802  esumcst  34806  esumfsup  34813  esumpcvgval  34821  esumcvg  34829  sigaclcuni  34861  mbfmfun  34997  dya2icoseg2  35021  bnj66  35601  bnj517  35626  dfk12  36053  dfk22  36054  dfk32  36055  cusgr3cyclex  36109  rellysconn  36224  cvmliftlem15  36271  satffunlem2lem1  36377  r1peuqusdeg1  36616  dfrdg4  36930  brcolinear2  37038  brcolinear  37039  ellines  37132  poimirlem29  38835  volsupnfl  38851  unirep  38916  filbcmb  38940  islshpkrN  40443  ispointN  41065  pmapglbx  41092  elsetpreimafvbi  48746  cycldlenngric  49299  grtrif1o  49313