Theorem rexlimiva 3129

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 3061	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
2		rexlimiva.1	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓)
3	2	exlimiv 1931	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓)
4	1, 3	sylbi 217	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1780   ∈ wcel 2113  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-ex 1781  df-rex 3061

This theorem is referenced by:  rexlimiv  3130  rexlimivw  3133  rexraleqim  3601  rexopabb  5476  unon  7773  tfrlem16  8324  oawordeulem  8481  nneob  8584  unfi  9095  ominf  9164  unfilem1  9205  fival  9315  elfi2  9317  fi0  9323  fiin  9325  djuss  9832  djuun  9838  updjud  9846  finnum  9860  dif1card  9920  fseqenlem2  9935  dfac8alem  9939  alephfp  10018  cflim2  10173  isfin1-3  10296  fin67  10305  isfin7-2  10306  axdc3lem  10360  axdc3lem2  10361  iunfo  10449  iundom2g  10450  winainflem  10604  rankcf  10688  map2psrpr  11021  supsrlem  11022  1re  11132  0re  11134  00id  11308  addrid  11313  0cnALT  11368  om2uzrani  13875  uzrdgfni  13881  wrdf  14441  rexanuz  15269  r19.2uz  15275  fsum2dlem  15693  fsumcom2  15697  fprod2dlem  15903  fprodcom2  15907  0dvds  16203  even2n  16269  m1expe  16301  m1exp1  16303  modprm0  16733  cshwsidrepsw  17021  smndex1basss  18830  smndex1mgm  18832  smndex1mndlem  18834  dfgrp2  18892  pzriprnglem4  21439  psgndiflemA  21556  ppttop  22951  epttop  22953  neips  23057  lmmo  23324  2ndctop  23391  2ndcsep  23403  fbncp  23783  fgcl  23822  filuni  23829  tgioo  24740  zcld  24758  cphsscph  25207  elovolm  25432  nulmbl2  25493  ellimc3  25836  limcflf  25838  pilem3  26419  perfect  27198  2vmadivsum  27508  selberg3lem2  27525  selberg4  27528  pntrsumbnd2  27534  pntrlog2bndlem3  27546  pntrlog2bndlem4  27547  pntpbnd  27555  pnt3  27579  elnoOLD  27614  noreson  27628  nosupbnd1lem5  27680  noinfbnd1lem5  27695  axcontlem12  29048  axcont  29049  clwwlkn1loopb  30118  eleclclwwlkn  30151  uhgr3cyclex  30257  frgrreggt1  30468  norm1exi  31325  nmcexi  32101  lnconi  32108  pjssdif1i  32250  stri  32332  hstri  32340  stcltrthi  32353  shatomici  32433  qsxpid  33443  dispcmp  34016  isrnmeas  34357  dya2iocucvr  34441  sxbrsigalem1  34442  eulerpartlemt  34528  bnj1398  35190  bnj1498  35217  fnrelpredd  35247  r1omfi  35261  wevgblacfn  35303  satfrnmapom  35564  gonar  35589  goalr  35591  satffun  35603  mthmblem  35774  lindsdom  37815  mblfinlem3  37860  ismblfin  37862  volsupnfl  37866  itg2addnclem  37872  itg2addnc  37875  cover2  37916  prtlem16  39139  rexzrexnn0  43056  isnumbasgrplem2  43356  dgraalem  43397  onsucrn  43523  dflim5  43581  dfno2  43679  rp-isfinite5  43768  mnurndlem1  44532  grumnudlem  44536  gruex  44549  islptre  45875  stirlinglem13  46340  stirlinglem14  46341  stirling  46343  etransc  46537  ovolval4lem2  46904  sprsymrelf1lem  47747  sprsymrelfolem2  47749  prmdvdsfmtnof  47842  prmdvdsfmtnof1  47843  perfectALTV  47979  tgoldbach  48073  uspgrsprf  48402  2zlidl  48496  2zrngamgm  48501  ply1mulgsumlem1  48642  ply1mulgsumlem2  48643  lincsumcl  48687  lincscmcl  48688  ellcoellss  48691  sepfsepc  49183  seppcld  49185