Theorem rexlimiva 3147

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

Syntax hints:   → wi 4   ∧ wa 396  ∃wex 1781   ∈ wcel 2106  ∃wrex 3070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-ex 1782  df-rex 3071

This theorem is referenced by:  rexlimiv  3148  rexlimivw  3151  rexraleqim  3634  rexopabb  5527  unon  7815  tfrlem16  8389  oawordeulem  8550  nneob  8651  unfi  9168  ominf  9254  ominfOLD  9255  unfilem1  9306  pwfiOLD  9343  fival  9403  elfi2  9405  fi0  9411  fiin  9413  djuss  9911  djuun  9917  updjud  9925  finnum  9939  dif1card  10001  fseqenlem2  10016  dfac8alem  10020  alephfp  10099  cflim2  10254  isfin1-3  10377  fin67  10386  isfin7-2  10387  axdc3lem  10441  axdc3lem2  10442  iunfo  10530  iundom2g  10531  winainflem  10684  rankcf  10768  map2psrpr  11101  supsrlem  11102  1re  11210  0re  11212  00id  11385  addrid  11390  0cnALT  11444  om2uzrani  13913  uzrdgfni  13919  wrdf  14465  rexanuz  15288  r19.2uz  15294  fsum2dlem  15712  fsumcom2  15716  fprod2dlem  15920  fprodcom2  15924  0dvds  16216  even2n  16281  m1expe  16313  m1exp1  16315  modprm0  16734  cshwsidrepsw  17023  smndex1basss  18782  smndex1mgm  18784  smndex1mndlem  18786  dfgrp2  18843  psgndiflemA  21145  ppttop  22501  epttop  22503  neips  22608  lmmo  22875  2ndctop  22942  2ndcsep  22954  fbncp  23334  fgcl  23373  filuni  23380  tgioo  24303  zcld  24320  cphsscph  24759  elovolm  24983  nulmbl2  25044  ellimc3  25387  limcflf  25389  pilem3  25956  perfect  26723  2vmadivsum  27033  selberg3lem2  27050  selberg4  27053  pntrsumbnd2  27059  pntrlog2bndlem3  27071  pntrlog2bndlem4  27072  pntpbnd  27080  pnt3  27104  elno  27138  noreson  27152  nosupbnd1lem5  27204  noinfbnd1lem5  27219  axcontlem12  28222  axcont  28223  clwwlkn1loopb  29285  eleclclwwlkn  29318  uhgr3cyclex  29424  frgrreggt1  29635  norm1exi  30490  nmcexi  31266  lnconi  31273  pjssdif1i  31415  stri  31497  hstri  31505  stcltrthi  31518  shatomici  31598  qsxpid  32462  dispcmp  32827  isrnmeas  33186  dya2iocucvr  33271  sxbrsigalem1  33272  eulerpartlemt  33358  bnj1398  34033  bnj1498  34060  fnrelpredd  34080  satfrnmapom  34349  gonar  34374  goalr  34376  satffun  34388  mthmblem  34559  lindsdom  36470  mblfinlem3  36515  ismblfin  36517  volsupnfl  36521  itg2addnclem  36527  itg2addnc  36530  cover2  36571  prtlem16  37727  rexzrexnn0  41527  isnumbasgrplem2  41831  dgraalem  41872  onsucrn  42006  dflim5  42064  dfno2  42164  rp-isfinite5  42253  mnurndlem1  43025  grumnudlem  43029  gruex  43042  islptre  44321  stirlinglem13  44788  stirlinglem14  44789  stirling  44791  etransc  44985  ovolval4lem2  45352  sprsymrelf1lem  46145  sprsymrelfolem2  46147  prmdvdsfmtnof  46240  prmdvdsfmtnof1  46241  perfectALTV  46377  tgoldbach  46471  uspgrsprf  46510  2zlidl  46785  2zrngamgm  46790  ply1mulgsumlem1  47020  ply1mulgsumlem2  47021  lincsumcl  47065  lincscmcl  47066  ellcoellss  47069  sepfsepc  47513  seppcld  47515