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  6943  fvelimab  6955  iinpreima  7067  fmpt  7108  fliftfun  7318  elrnmpo  7554  ovelrn  7595  onuninsuci  7849  fiunlem  7952  releldm2  8052  poxp2  8153  poxp3  8160  orderseqlem  8167  tfrlem4  8379  naddunif  8696  iiner  8803  elixpsn  8958  isfi  8995  card2on  9541  brttrcl  9707  tz9.12lem1  9787  rankwflemb  9793  rankwflembOLD  9794  rankxpsuc  9892  scott0b  9930  scott0OLD  9931  isnum2  10019  cardiun  10056  cardalephex  10162  dfac5lem4  10198  dfac12k  10219  cflim2  10334  cfss  10336  cfslb2n  10339  enfin2i  10392  fin23lem30  10413  itunitc  10492  axdc3lem2  10522  iundom2g  10617  pwcfsdom  10661  cfpwsdom  10662  tskhf  10846  genpelv  11078  prlem934  11111  suplem1pr  11130  supexpr  11132  supsrlem  11189  supsr  11190  fimaxre3  12256  iswrd  14653  caurcvgr  15834  caurcvg  15837  caucvg  15839  vdwapval  17144  restsspw  17595  mreunirn  17764  brssc  17982  arwhoma  18213  gexcl3  19794  dvdsr  20585  rhmdvdsr  20751  ellspsn  21271  lspprel  21362  ellspd  22101  iincld  23350  ssnei  23421  neindisj2  23434  neitr  23491  lecldbas  23530  tgcnp  23564  cncnp2  23592  lmmo  23691  is2ndc  23757  fbfinnfr  24153  fbunfip  24181  filunirn  24194  fbflim2  24289  flimcls  24297  hauspwpwf1  24299  flftg  24308  isfcls  24321  fclsbas  24333  isfcf  24346  ustfilxp  24525  ustbas  24539  restutop  24549  ucnima  24592  xmetunirn  24649  metss  24820  metrest  24836  restmetu  24882  qdensere  25081  elpi1  25359  lmmbr  25572  caun0  25595  nulmbl2  25850  itg2l  26043  aannenlem2  26649  taylfval  26679  ulmcl  26701  ulmpm  26703  ulmss  26717  elno  27996  nofun  27999  norn  28001  madeval2  28212  elmade  28236  tglnunirn  29004  ishpg  29230  edglnl  29714  uhgrwkspthlem1  30332  usgr2pth  30343  umgr2wlk  30531  elwwlks2ons3  30537  clwwlknun  30696  frgrncvvdeqlem3  30895  frgr2wwlkn0  30922  frgrreg  30988  hhcms  31798  hhsscms  31873  occllem  31898  occl  31899  chscllem2  32233  r19.29ffa  33061  rabfmpunirn  33240  kerunit  33879  tpr2rico  34537  gsumesum  34684  esumcst  34688  esumfsup  34695  esumpcvgval  34703  esumcvg  34711  sigaclcuni  34743  mbfmfun  34879  dya2icoseg2  34903  bnj66  35483  bnj517  35508  cusgr3cyclex  35890  rellysconn  35995  cvmliftlem15  36042  satffunlem2lem1  36148  r1peuqusdeg1  36387  dfrdg4  36695  brcolinear2  36803  brcolinear  36804  ellines  36897  poimirlem29  38547  volsupnfl  38563  unirep  38628  filbcmb  38654  islshpkrN  40157  ispointN  40779  pmapglbx  40806  rngunsnply  44155  elsetpreimafvbi  48442  cycldlenngric  48995  grtrif1o  49009