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 2144  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-rex 3087

This theorem is used by:  r19.36v  3190  r19.45v  3196  r19.44v  3197  sbcreu  3823  eliun  4954  reusv3i  5366  elrnmptg  5944  fvelrnb  6950  fvelimab  6962  iinpreima  7074  fmpt  7115  fliftfun  7324  elrnmpo  7560  ovelrn  7601  onuninsuci  7855  fiunlem  7958  releldm2  8058  poxp2  8166  poxp3  8173  orderseqlem  8180  tfrlem4  8393  naddunif  8710  iiner  8817  elixpsn  8972  isfi  9009  card2on  9555  brttrcl  9721  tz9.12lem1  9801  rankwflemb  9807  rankwflembOLD  9808  rankxpsuc  9906  scott0b  9944  scott0OLD  9945  isnum2  10033  cardiun  10070  cardalephex  10176  dfac5lem4  10212  dfac12k  10233  cflim2  10348  cfss  10350  cfslb2n  10353  enfin2i  10406  fin23lem30  10427  itunitc  10506  axdc3lem2  10536  iundom2g  10631  pwcfsdom  10675  cfpwsdom  10676  tskhf  10860  genpelv  11092  prlem934  11125  suplem1pr  11144  supexpr  11146  supsrlem  11203  supsr  11204  fimaxre3  12270  iswrd  14667  caurcvgr  15850  caurcvg  15853  caucvg  15855  vdwapval  17160  restsspw  17611  mreunirn  17780  brssc  17998  arwhoma  18229  gexcl3  19810  dvdsr  20601  rhmdvdsr  20767  ellspsn  21287  lspprel  21378  ellspd  22117  iincld  23366  ssnei  23437  neindisj2  23450  neitr  23507  lecldbas  23546  tgcnp  23580  cncnp2  23608  lmmo  23707  is2ndc  23773  fbfinnfr  24169  fbunfip  24197  filunirn  24210  fbflim2  24305  flimcls  24313  hauspwpwf1  24315  flftg  24324  isfcls  24337  fclsbas  24349  isfcf  24362  ustfilxp  24541  ustbas  24555  restutop  24565  ucnima  24608  xmetunirn  24665  metss  24836  metrest  24852  restmetu  24898  qdensere  25097  elpi1  25375  lmmbr  25588  caun0  25611  nulmbl2  25866  itg2l  26059  aannenlem2  26665  taylfval  26695  ulmcl  26717  ulmpm  26719  ulmss  26733  elno  28012  nofun  28015  norn  28017  madeval2  28228  elmade  28252  tglnunirn  29020  ishpg  29246  edglnl  29730  uhgrwkspthlem1  30348  usgr2pth  30359  umgr2wlk  30547  elwwlks2ons3  30553  clwwlknun  30712  frgrncvvdeqlem3  30911  frgr2wwlkn0  30938  frgrreg  31004  hhcms  31814  hhsscms  31889  occllem  31914  occl  31915  chscllem2  32249  r19.29ffa  33119  rabfmpunirn  33298  kerunit  33936  tpr2rico  34594  gsumesum  34741  esumcst  34745  esumfsup  34752  esumpcvgval  34760  esumcvg  34768  sigaclcuni  34800  mbfmfun  34936  dya2icoseg2  34960  bnj66  35540  bnj517  35565  cusgr3cyclex  35991  rellysconn  36106  cvmliftlem15  36153  satffunlem2lem1  36259  r1peuqusdeg1  36498  dfrdg4  36811  brcolinear2  36919  brcolinear  36920  ellines  37013  poimirlem29  38676  volsupnfl  38692  unirep  38757  filbcmb  38783  islshpkrN  40286  ispointN  40908  pmapglbx  40935  rngunsnply  44280  elsetpreimafvbi  48581  cycldlenngric  49134  grtrif1o  49148