Theorem rexlimivw 3160

Description: Weaker version of rexlimiv 3157. (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 3156	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ∃wrex 3087

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 1943

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

This theorem is used by:  r19.36v  3191  r19.45v  3197  r19.44v  3198  sbcreu  3823  eliun  4955  reusv3i  5366  elrnmptg  5943  fvelrnb  6946  fvelimab  6958  iinpreima  7070  fmpt  7111  fliftfun  7321  elrnmpo  7557  ovelrn  7598  onuninsuci  7852  fiunlem  7955  releldm2  8055  poxp2  8161  poxp3  8168  orderseqlem  8175  tfrlem4  8387  naddunif  8704  iiner  8811  elixpsn  8966  isfi  9003  card2on  9549  brttrcl  9715  tz9.12lem1  9795  rankwflemb  9801  rankwflembOLD  9802  rankxpsuc  9900  scott0b  9938  scott0OLD  9939  isnum2  10027  cardiun  10064  cardalephex  10170  dfac5lem4  10206  dfac12k  10227  cflim2  10342  cfss  10344  cfslb2n  10347  enfin2i  10400  fin23lem30  10421  itunitc  10500  axdc3lem2  10530  iundom2g  10625  pwcfsdom  10669  cfpwsdom  10670  tskhf  10854  genpelv  11086  prlem934  11119  suplem1pr  11138  supexpr  11140  supsrlem  11197  supsr  11198  fimaxre3  12264  iswrd  14661  caurcvgr  15842  caurcvg  15845  caucvg  15847  vdwapval  17152  restsspw  17603  mreunirn  17772  brssc  17990  arwhoma  18221  gexcl3  19802  dvdsr  20593  rhmdvdsr  20759  ellspsn  21279  lspprel  21370  ellspd  22109  iincld  23358  ssnei  23429  neindisj2  23442  neitr  23499  lecldbas  23538  tgcnp  23572  cncnp2  23600  lmmo  23699  is2ndc  23765  fbfinnfr  24161  fbunfip  24189  filunirn  24202  fbflim2  24297  flimcls  24305  hauspwpwf1  24307  flftg  24316  isfcls  24329  fclsbas  24341  isfcf  24354  ustfilxp  24533  ustbas  24547  restutop  24557  ucnima  24600  xmetunirn  24657  metss  24828  metrest  24844  restmetu  24890  qdensere  25089  elpi1  25367  lmmbr  25580  caun0  25603  nulmbl2  25858  itg2l  26051  aannenlem2  26657  taylfval  26687  ulmcl  26709  ulmpm  26711  ulmss  26725  elno  28004  nofun  28007  norn  28009  madeval2  28220  elmade  28244  tglnunirn  29012  ishpg  29238  edglnl  29722  uhgrwkspthlem1  30340  usgr2pth  30351  umgr2wlk  30539  elwwlks2ons3  30545  clwwlknun  30704  frgrncvvdeqlem3  30903  frgr2wwlkn0  30930  frgrreg  30996  hhcms  31806  hhsscms  31881  occllem  31906  occl  31907  chscllem2  32241  r19.29ffa  33069  rabfmpunirn  33248  kerunit  33887  tpr2rico  34545  gsumesum  34692  esumcst  34696  esumfsup  34703  esumpcvgval  34711  esumcvg  34719  sigaclcuni  34751  mbfmfun  34887  dya2icoseg2  34911  bnj66  35491  bnj517  35516  cusgr3cyclex  35912  rellysconn  36017  cvmliftlem15  36064  satffunlem2lem1  36170  r1peuqusdeg1  36409  dfrdg4  36716  brcolinear2  36824  brcolinear  36825  ellines  36918  poimirlem29  38569  volsupnfl  38585  unirep  38650  filbcmb  38676  islshpkrN  40179  ispointN  40801  pmapglbx  40828  rngunsnply  44172  elsetpreimafvbi  48474  cycldlenngric  49027  grtrif1o  49041