Theorem rexlimiva 3144

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1775   ∈ wcel 2105  ∃wrex 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907

This theorem depends on definitions:  df-bi 207  df-ex 1776  df-rex 3068

This theorem is referenced by:  rexlimiv  3145  rexlimivw  3148  rexraleqim  3646  rexopabb  5537  unon  7850  tfrlem16  8431  oawordeulem  8590  nneob  8692  unfi  9209  ominf  9291  ominfOLD  9292  unfilem1  9340  fival  9449  elfi2  9451  fi0  9457  fiin  9459  djuss  9957  djuun  9963  updjud  9971  finnum  9985  dif1card  10047  fseqenlem2  10062  dfac8alem  10066  alephfp  10145  cflim2  10300  isfin1-3  10423  fin67  10432  isfin7-2  10433  axdc3lem  10487  axdc3lem2  10488  iunfo  10576  iundom2g  10577  winainflem  10730  rankcf  10814  map2psrpr  11147  supsrlem  11148  1re  11258  0re  11260  00id  11433  addrid  11438  0cnALT  11493  om2uzrani  13989  uzrdgfni  13995  wrdf  14553  rexanuz  15380  r19.2uz  15386  fsum2dlem  15802  fsumcom2  15806  fprod2dlem  16012  fprodcom2  16016  0dvds  16310  even2n  16375  m1expe  16407  m1exp1  16409  modprm0  16838  cshwsidrepsw  17127  smndex1basss  18930  smndex1mgm  18932  smndex1mndlem  18934  dfgrp2  18992  pzriprnglem4  21512  psgndiflemA  21636  ppttop  23029  epttop  23031  neips  23136  lmmo  23403  2ndctop  23470  2ndcsep  23482  fbncp  23862  fgcl  23901  filuni  23908  tgioo  24831  zcld  24848  cphsscph  25298  elovolm  25523  nulmbl2  25584  ellimc3  25928  limcflf  25930  pilem3  26511  perfect  27289  2vmadivsum  27599  selberg3lem2  27616  selberg4  27619  pntrsumbnd2  27625  pntrlog2bndlem3  27637  pntrlog2bndlem4  27638  pntpbnd  27646  pnt3  27670  elnoOLD  27705  noreson  27719  nosupbnd1lem5  27771  noinfbnd1lem5  27786  axcontlem12  29004  axcont  29005  clwwlkn1loopb  30071  eleclclwwlkn  30104  uhgr3cyclex  30210  frgrreggt1  30421  norm1exi  31278  nmcexi  32054  lnconi  32061  pjssdif1i  32203  stri  32285  hstri  32293  stcltrthi  32306  shatomici  32386  qsxpid  33369  dispcmp  33819  isrnmeas  34180  dya2iocucvr  34265  sxbrsigalem1  34266  eulerpartlemt  34352  bnj1398  35026  bnj1498  35053  fnrelpredd  35081  wevgblacfn  35092  satfrnmapom  35354  gonar  35379  goalr  35381  satffun  35393  mthmblem  35564  lindsdom  37600  mblfinlem3  37645  ismblfin  37647  volsupnfl  37651  itg2addnclem  37657  itg2addnc  37660  cover2  37701  prtlem16  38850  rexzrexnn0  42791  isnumbasgrplem2  43092  dgraalem  43133  onsucrn  43260  dflim5  43318  dfno2  43417  rp-isfinite5  43506  mnurndlem1  44276  grumnudlem  44280  gruex  44293  islptre  45574  stirlinglem13  46041  stirlinglem14  46042  stirling  46044  etransc  46238  ovolval4lem2  46605  sprsymrelf1lem  47415  sprsymrelfolem2  47417  prmdvdsfmtnof  47510  prmdvdsfmtnof1  47511  perfectALTV  47647  tgoldbach  47741  uspgrsprf  47989  2zlidl  48083  2zrngamgm  48088  ply1mulgsumlem1  48231  ply1mulgsumlem2  48232  lincsumcl  48276  lincscmcl  48277  ellcoellss  48280  sepfsepc  48723  seppcld  48725