Theorem rexlimivw 3137

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

Syntax hints:   → wi 4   ∈ wcel 2108  ∃wrex 3060

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 3061

This theorem is referenced by:  r19.36v  3169  r19.45v  3178  r19.44v  3179  sbcreu  3851  eliun  4971  reusv3i  5374  elrnmptg  5941  fvelrnb  6938  fvelimab  6950  iinpreima  7058  fmpt  7099  fliftfun  7304  elrnmpo  7541  ovelrn  7581  onuninsuci  7833  fiunlem  7938  releldm2  8040  poxp2  8140  poxp3  8147  orderseqlem  8154  tfrlem4  8391  naddunif  8703  iiner  8801  elixpsn  8949  isfi  8988  card2on  9566  brttrcl  9725  tz9.12lem1  9799  rankwflemb  9805  rankxpsuc  9894  scott0  9898  isnum2  9957  cardiun  9994  cardalephex  10102  dfac5lem4  10138  dfac5lem4OLD  10140  dfac12k  10160  cflim2  10275  cfss  10277  cfslb2n  10280  enfin2i  10333  fin23lem30  10354  itunitc  10433  axdc3lem2  10463  iundom2g  10552  pwcfsdom  10595  cfpwsdom  10596  tskr1om2  10780  genpelv  11012  prlem934  11045  suplem1pr  11064  supexpr  11066  supsrlem  11123  supsr  11124  fimaxre3  12186  iswrd  14531  caurcvgr  15688  caurcvg  15691  caucvg  15693  vdwapval  16991  restsspw  17443  mreunirn  17611  brssc  17825  arwhoma  18056  gexcl3  19566  dvdsr  20320  rhmdvdsr  20466  ellspsn  20958  lspprel  21050  ellspd  21760  iincld  22975  ssnei  23046  neindisj2  23059  neitr  23116  lecldbas  23155  tgcnp  23189  cncnp2  23217  lmmo  23316  is2ndc  23382  fbfinnfr  23777  fbunfip  23805  filunirn  23818  fbflim2  23913  flimcls  23921  hauspwpwf1  23923  flftg  23932  isfcls  23945  fclsbas  23957  isfcf  23970  ustfilxp  24149  ustbas  24164  restutop  24174  ucnima  24217  xmetunirn  24274  metss  24445  metrest  24461  restmetu  24507  qdensere  24706  elpi1  24994  lmmbr  25208  caun0  25231  nulmbl2  25487  itg2l  25680  aannenlem2  26287  taylfval  26316  ulmcl  26340  ulmpm  26342  ulmss  26356  elno  27607  nofun  27611  norn  27613  madeval2  27809  elmade  27823  tglnunirn  28473  ishpg  28684  edglnl  29068  uhgrwkspthlem1  29681  usgr2pth  29692  umgr2wlk  29877  elwwlks2ons3  29883  clwwlknun  30039  frgrncvvdeqlem3  30228  frgr2wwlkn0  30255  frgrreg  30321  hhcms  31130  hhsscms  31205  occllem  31230  occl  31231  chscllem2  31565  r19.29ffa  32398  rabfmpunirn  32577  kerunit  33287  tpr2rico  33889  gsumesum  34036  esumcst  34040  esumfsup  34047  esumpcvgval  34055  esumcvg  34063  sigaclcuni  34095  mbfmfun  34230  dya2icoseg2  34256  bnj66  34837  bnj517  34862  cusgr3cyclex  35104  rellysconn  35219  cvmliftlem15  35266  satffunlem2lem1  35372  r1peuqusdeg1  35611  dfrdg4  35915  brcolinear2  36022  brcolinear  36023  ellines  36116  poimirlem29  37619  volsupnfl  37635  unirep  37684  filbcmb  37710  islshpkrN  39084  ispointN  39707  pmapglbx  39734  rngunsnply  43140  elsetpreimafvbi  47353  cycldlenngric  47889  grtrif1o  47902