Theorem rexlimivw 3134

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

Syntax hints:   → wi 4   ∈ wcel 2114  ∃wrex 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3062

This theorem is referenced by:  r19.36v  3165  r19.45v  3171  r19.44v  3172  sbcreu  3814  eliun  4937  reusv3i  5346  elrnmptg  5916  fvelrnb  6900  fvelimab  6912  iinpreima  7021  fmpt  7062  fliftfun  7267  elrnmpo  7503  ovelrn  7543  onuninsuci  7791  fiunlem  7895  releldm2  7996  poxp2  8093  poxp3  8100  orderseqlem  8107  tfrlem4  8318  naddunif  8629  iiner  8736  elixpsn  8885  isfi  8922  card2on  9469  brttrcl  9634  tz9.12lem1  9711  rankwflemb  9717  rankxpsuc  9806  scott0  9810  isnum2  9869  cardiun  9906  cardalephex  10012  dfac5lem4  10048  dfac5lem4OLD  10050  dfac12k  10070  cflim2  10185  cfss  10187  cfslb2n  10190  enfin2i  10243  fin23lem30  10264  itunitc  10343  axdc3lem2  10373  iundom2g  10462  pwcfsdom  10506  cfpwsdom  10507  tskr1om2  10691  genpelv  10923  prlem934  10956  suplem1pr  10975  supexpr  10977  supsrlem  11034  supsr  11035  fimaxre3  12102  iswrd  14477  caurcvgr  15636  caurcvg  15639  caucvg  15641  vdwapval  16944  restsspw  17394  mreunirn  17563  brssc  17781  arwhoma  18012  gexcl3  19562  dvdsr  20342  rhmdvdsr  20485  ellspsn  20998  lspprel  21089  ellspd  21782  iincld  23004  ssnei  23075  neindisj2  23088  neitr  23145  lecldbas  23184  tgcnp  23218  cncnp2  23246  lmmo  23345  is2ndc  23411  fbfinnfr  23806  fbunfip  23834  filunirn  23847  fbflim2  23942  flimcls  23950  hauspwpwf1  23952  flftg  23961  isfcls  23974  fclsbas  23986  isfcf  23999  ustfilxp  24178  ustbas  24192  restutop  24202  ucnima  24245  xmetunirn  24302  metss  24473  metrest  24489  restmetu  24535  qdensere  24734  elpi1  25012  lmmbr  25225  caun0  25248  nulmbl2  25503  itg2l  25696  aannenlem2  26295  taylfval  26324  ulmcl  26346  ulmpm  26348  ulmss  26362  elno  27609  nofun  27613  norn  27615  madeval2  27825  elmade  27849  tglnunirn  28616  ishpg  28827  edglnl  29212  uhgrwkspthlem1  29821  usgr2pth  29832  umgr2wlk  30017  elwwlks2ons3  30023  clwwlknun  30182  frgrncvvdeqlem3  30371  frgr2wwlkn0  30398  frgrreg  30464  hhcms  31274  hhsscms  31349  occllem  31374  occl  31375  chscllem2  31709  r19.29ffa  32540  rabfmpunirn  32726  kerunit  33385  tpr2rico  34056  gsumesum  34203  esumcst  34207  esumfsup  34214  esumpcvgval  34222  esumcvg  34230  sigaclcuni  34262  mbfmfun  34397  dya2icoseg2  34422  bnj66  35002  bnj517  35027  cusgr3cyclex  35318  rellysconn  35433  cvmliftlem15  35480  satffunlem2lem1  35586  r1peuqusdeg1  35825  dfrdg4  36133  brcolinear2  36240  brcolinear  36241  ellines  36334  poimirlem29  37970  volsupnfl  37986  unirep  38035  filbcmb  38061  islshpkrN  39566  ispointN  40188  pmapglbx  40215  rngunsnply  43597  elsetpreimafvbi  47851  cycldlenngric  48404  grtrif1o  48418