Theorem rexlimiva 3131

Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 18-Dec-2006.) Shorten dependent theorems. (Revised by Wolf lammen, 23-Dec-2024.)

Hypothesis

Ref	Expression
rexlimiva.1	⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓)

Assertion

Ref	Expression
rexlimiva	⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

Distinct variable group:   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥)

Proof of Theorem rexlimiva

Step	Hyp	Ref	Expression
1		df-rex 3060	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
2		rexlimiva.1	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓)
3	2	exlimiv 1929	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓)
4	1, 3	sylbi 217	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1778   ∈ wcel 2107  ∃wrex 3059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-ex 1779  df-rex 3060

This theorem is referenced by:  rexlimiv  3132  rexlimivw  3135  rexraleqim  3624  rexopabb  5500  unon  7819  tfrlem16  8401  oawordeulem  8560  nneob  8662  unfi  9179  ominf  9260  ominfOLD  9261  unfilem1  9309  fival  9418  elfi2  9420  fi0  9426  fiin  9428  djuss  9926  djuun  9932  updjud  9940  finnum  9954  dif1card  10016  fseqenlem2  10031  dfac8alem  10035  alephfp  10114  cflim2  10269  isfin1-3  10392  fin67  10401  isfin7-2  10402  axdc3lem  10456  axdc3lem2  10457  iunfo  10545  iundom2g  10546  winainflem  10699  rankcf  10783  map2psrpr  11116  supsrlem  11117  1re  11227  0re  11229  00id  11402  addrid  11407  0cnALT  11462  om2uzrani  13959  uzrdgfni  13965  wrdf  14524  rexanuz  15351  r19.2uz  15357  fsum2dlem  15773  fsumcom2  15777  fprod2dlem  15983  fprodcom2  15987  0dvds  16281  even2n  16346  m1expe  16378  m1exp1  16380  modprm0  16810  cshwsidrepsw  17098  smndex1basss  18868  smndex1mgm  18870  smndex1mndlem  18872  dfgrp2  18930  pzriprnglem4  21430  psgndiflemA  21546  ppttop  22930  epttop  22932  neips  23036  lmmo  23303  2ndctop  23370  2ndcsep  23382  fbncp  23762  fgcl  23801  filuni  23808  tgioo  24720  zcld  24738  cphsscph  25188  elovolm  25413  nulmbl2  25474  ellimc3  25817  limcflf  25819  pilem3  26400  perfect  27178  2vmadivsum  27488  selberg3lem2  27505  selberg4  27508  pntrsumbnd2  27514  pntrlog2bndlem3  27526  pntrlog2bndlem4  27527  pntpbnd  27535  pnt3  27559  elnoOLD  27594  noreson  27608  nosupbnd1lem5  27660  noinfbnd1lem5  27675  axcontlem12  28886  axcont  28887  clwwlkn1loopb  29956  eleclclwwlkn  29989  uhgr3cyclex  30095  frgrreggt1  30306  norm1exi  31163  nmcexi  31939  lnconi  31946  pjssdif1i  32088  stri  32170  hstri  32178  stcltrthi  32191  shatomici  32271  qsxpid  33295  dispcmp  33798  isrnmeas  34139  dya2iocucvr  34224  sxbrsigalem1  34225  eulerpartlemt  34311  bnj1398  34986  bnj1498  35013  fnrelpredd  35041  wevgblacfn  35052  satfrnmapom  35313  gonar  35338  goalr  35340  satffun  35352  mthmblem  35523  lindsdom  37559  mblfinlem3  37604  ismblfin  37606  volsupnfl  37610  itg2addnclem  37616  itg2addnc  37619  cover2  37660  prtlem16  38808  rexzrexnn0  42752  isnumbasgrplem2  43053  dgraalem  43094  onsucrn  43220  dflim5  43278  dfno2  43377  rp-isfinite5  43466  mnurndlem1  44231  grumnudlem  44235  gruex  44248  islptre  45578  stirlinglem13  46045  stirlinglem14  46046  stirling  46048  etransc  46242  ovolval4lem2  46609  sprsymrelf1lem  47423  sprsymrelfolem2  47425  prmdvdsfmtnof  47518  prmdvdsfmtnof1  47519  perfectALTV  47655  tgoldbach  47749  uspgrsprf  48007  2zlidl  48101  2zrngamgm  48106  ply1mulgsumlem1  48248  ply1mulgsumlem2  48249  lincsumcl  48293  lincscmcl  48294  ellcoellss  48297  sepfsepc  48781  seppcld  48783