Theorem rexlimivw 3159

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

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

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 3087

This theorem is used by:  r19.36v  3190  r19.45v  3196  r19.44v  3197  sbcreu  3823  eliun  4955  reusv3i  5369  elrnmptg  5945  fvelrnb  6938  fvelimab  6950  iinpreima  7062  fmpt  7103  fliftfun  7313  elrnmpo  7549  ovelrn  7590  onuninsuci  7836  fiunlem  7939  releldm2  8040  poxp2  8141  poxp3  8148  orderseqlem  8155  tfrlem4  8367  naddunif  8682  iiner  8789  elixpsn  8944  isfi  8981  card2on  9526  brttrcl  9692  tz9.12lem1  9769  rankwflemb  9775  rankxpsuc  9864  scott0b  9876  scott0OLD  9877  isnum2  9950  cardiun  9987  cardalephex  10093  dfac5lem4  10129  dfac12k  10150  cflim2  10265  cfss  10267  cfslb2n  10270  enfin2i  10323  fin23lem30  10344  itunitc  10423  axdc3lem2  10453  iundom2g  10548  pwcfsdom  10592  cfpwsdom  10593  tskr1om2  10777  genpelv  11009  prlem934  11042  suplem1pr  11061  supexpr  11063  supsrlem  11120  supsr  11121  fimaxre3  12185  iswrd  14580  caurcvgr  15761  caurcvg  15764  caucvg  15766  vdwapval  17065  restsspw  17516  mreunirn  17685  brssc  17903  arwhoma  18134  gexcl3  19714  dvdsr  20503  rhmdvdsr  20668  ellspsn  21187  lspprel  21278  ellspd  22015  iincld  23264  ssnei  23335  neindisj2  23348  neitr  23405  lecldbas  23444  tgcnp  23478  cncnp2  23506  lmmo  23605  is2ndc  23671  fbfinnfr  24067  fbunfip  24095  filunirn  24108  fbflim2  24203  flimcls  24211  hauspwpwf1  24213  flftg  24222  isfcls  24235  fclsbas  24247  isfcf  24260  ustfilxp  24439  ustbas  24453  restutop  24463  ucnima  24506  xmetunirn  24563  metss  24734  metrest  24750  restmetu  24796  qdensere  24995  elpi1  25273  lmmbr  25486  caun0  25509  nulmbl2  25764  itg2l  25957  aannenlem2  26565  taylfval  26595  ulmcl  26617  ulmpm  26619  ulmss  26633  elno  27882  nofun  27885  norn  27887  madeval2  28098  elmade  28122  tglnunirn  28890  ishpg  29116  edglnl  29600  uhgrwkspthlem1  30218  usgr2pth  30229  umgr2wlk  30417  elwwlks2ons3  30423  clwwlknun  30582  frgrncvvdeqlem3  30781  frgr2wwlkn0  30808  frgrreg  30874  hhcms  31684  hhsscms  31759  occllem  31784  occl  31785  chscllem2  32119  r19.29ffa  32947  rabfmpunirn  33126  kerunit  33765  tpr2rico  34422  gsumesum  34569  esumcst  34573  esumfsup  34580  esumpcvgval  34588  esumcvg  34596  sigaclcuni  34628  mbfmfun  34764  dya2icoseg2  34789  bnj66  35369  bnj517  35394  cusgr3cyclex  35725  rellysconn  35830  cvmliftlem15  35877  satffunlem2lem1  35983  r1peuqusdeg1  36222  dfrdg4  36530  brcolinear2  36638  brcolinear  36639  ellines  36732  poimirlem29  38398  volsupnfl  38414  unirep  38464  filbcmb  38490  islshpkrN  39993  ispointN  40615  pmapglbx  40642  rngunsnply  44010  elsetpreimafvbi  48291  cycldlenngric  48844  grtrif1o  48858