Theorem rexlimivw 3164

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ∃wrex 3091

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 3092

This theorem is used by:  r19.36v  3195  r19.45v  3201  r19.44v  3202  sbcreu  3830  eliun  4962  reusv3i  5377  elrnmptg  5953  fvelrnb  6945  fvelimab  6957  iinpreima  7068  fmpt  7109  fliftfun  7319  elrnmpo  7555  ovelrn  7596  onuninsuci  7842  fiunlem  7945  releldm2  8046  poxp2  8145  poxp3  8152  orderseqlem  8159  tfrlem4  8371  naddunif  8686  iiner  8793  elixpsn  8941  isfi  8978  card2on  9523  brttrcl  9689  tz9.12lem1  9766  rankwflemb  9772  rankxpsuc  9861  scott0b  9873  scott0OLD  9874  isnum2  9947  cardiun  9984  cardalephex  10090  dfac5lem4  10126  dfac12k  10147  cflim2  10262  cfss  10264  cfslb2n  10267  enfin2i  10320  fin23lem30  10341  itunitc  10420  axdc3lem2  10450  iundom2g  10539  pwcfsdom  10583  cfpwsdom  10584  tskr1om2  10768  genpelv  11000  prlem934  11033  suplem1pr  11052  supexpr  11054  supsrlem  11111  supsr  11112  fimaxre3  12176  iswrd  14570  caurcvgr  15749  caurcvg  15752  caucvg  15754  vdwapval  17055  restsspw  17506  mreunirn  17675  brssc  17893  arwhoma  18124  gexcl3  19701  dvdsr  20490  rhmdvdsr  20655  ellspsn  21174  lspprel  21265  ellspd  22002  iincld  23246  ssnei  23317  neindisj2  23330  neitr  23387  lecldbas  23426  tgcnp  23460  cncnp2  23488  lmmo  23587  is2ndc  23653  fbfinnfr  24049  fbunfip  24077  filunirn  24090  fbflim2  24185  flimcls  24193  hauspwpwf1  24195  flftg  24204  isfcls  24217  fclsbas  24229  isfcf  24242  ustfilxp  24421  ustbas  24435  restutop  24445  ucnima  24488  xmetunirn  24545  metss  24716  metrest  24732  restmetu  24778  qdensere  24977  elpi1  25255  lmmbr  25468  caun0  25491  nulmbl2  25746  itg2l  25939  aannenlem2  26543  taylfval  26573  ulmcl  26595  ulmpm  26597  ulmss  26611  elno  27861  nofun  27864  norn  27866  madeval2  28077  elmade  28101  tglnunirn  28868  ishpg  29092  edglnl  29548  uhgrwkspthlem1  30166  usgr2pth  30177  umgr2wlk  30365  elwwlks2ons3  30371  clwwlknun  30530  frgrncvvdeqlem3  30723  frgr2wwlkn0  30750  frgrreg  30816  hhcms  31626  hhsscms  31701  occllem  31726  occl  31727  chscllem2  32061  r19.29ffa  32889  rabfmpunirn  33069  kerunit  33709  tpr2rico  34366  gsumesum  34513  esumcst  34517  esumfsup  34524  esumpcvgval  34532  esumcvg  34540  sigaclcuni  34572  mbfmfun  34708  dya2icoseg2  34733  bnj66  35313  bnj517  35338  cusgr3cyclex  35669  rellysconn  35780  cvmliftlem15  35827  satffunlem2lem1  35933  r1peuqusdeg1  36172  dfrdg4  36480  brcolinear2  36587  brcolinear  36588  ellines  36681  poimirlem29  38357  volsupnfl  38373  unirep  38423  filbcmb  38449  islshpkrN  39952  ispointN  40574  pmapglbx  40601  rngunsnply  43954  elsetpreimafvbi  48198  cycldlenngric  48751  grtrif1o  48765