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  3635  rexopabb  5528  unon  7821  tfrlem16  8395  oawordeulem  8556  nneob  8657  unfi  9174  ominf  9260  ominfOLD  9261  unfilem1  9312  pwfiOLD  9349  fival  9409  elfi2  9411  fi0  9417  fiin  9419  djuss  9917  djuun  9923  updjud  9931  finnum  9945  dif1card  10007  fseqenlem2  10022  dfac8alem  10026  alephfp  10105  cflim2  10260  isfin1-3  10383  fin67  10392  isfin7-2  10393  axdc3lem  10447  axdc3lem2  10448  iunfo  10536  iundom2g  10537  winainflem  10690  rankcf  10774  map2psrpr  11107  supsrlem  11108  1re  11216  0re  11218  00id  11391  addrid  11396  0cnALT  11450  om2uzrani  13919  uzrdgfni  13925  wrdf  14471  rexanuz  15294  r19.2uz  15300  fsum2dlem  15718  fsumcom2  15722  fprod2dlem  15926  fprodcom2  15930  0dvds  16222  even2n  16287  m1expe  16319  m1exp1  16321  modprm0  16740  cshwsidrepsw  17029  smndex1basss  18788  smndex1mgm  18790  smndex1mndlem  18792  dfgrp2  18849  psgndiflemA  21160  ppttop  22517  epttop  22519  neips  22624  lmmo  22891  2ndctop  22958  2ndcsep  22970  fbncp  23350  fgcl  23389  filuni  23396  tgioo  24319  zcld  24336  cphsscph  24775  elovolm  24999  nulmbl2  25060  ellimc3  25403  limcflf  25405  pilem3  25972  perfect  26741  2vmadivsum  27051  selberg3lem2  27068  selberg4  27071  pntrsumbnd2  27077  pntrlog2bndlem3  27089  pntrlog2bndlem4  27090  pntpbnd  27098  pnt3  27122  elno  27156  noreson  27170  nosupbnd1lem5  27222  noinfbnd1lem5  27237  axcontlem12  28271  axcont  28272  clwwlkn1loopb  29334  eleclclwwlkn  29367  uhgr3cyclex  29473  frgrreggt1  29684  norm1exi  30541  nmcexi  31317  lnconi  31324  pjssdif1i  31466  stri  31548  hstri  31556  stcltrthi  31569  shatomici  31649  qsxpid  32519  dispcmp  32908  isrnmeas  33267  dya2iocucvr  33352  sxbrsigalem1  33353  eulerpartlemt  33439  bnj1398  34114  bnj1498  34141  fnrelpredd  34161  satfrnmapom  34430  gonar  34455  goalr  34457  satffun  34469  mthmblem  34640  lindsdom  36568  mblfinlem3  36613  ismblfin  36615  volsupnfl  36619  itg2addnclem  36625  itg2addnc  36628  cover2  36669  prtlem16  37825  rexzrexnn0  41624  isnumbasgrplem2  41928  dgraalem  41969  onsucrn  42103  dflim5  42161  dfno2  42261  rp-isfinite5  42350  mnurndlem1  43122  grumnudlem  43126  gruex  43139  islptre  44414  stirlinglem13  44881  stirlinglem14  44882  stirling  44884  etransc  45078  ovolval4lem2  45445  sprsymrelf1lem  46238  sprsymrelfolem2  46240  prmdvdsfmtnof  46333  prmdvdsfmtnof1  46334  perfectALTV  46470  tgoldbach  46564  uspgrsprf  46603  pzriprnglem4  46887  2zlidl  46911  2zrngamgm  46916  ply1mulgsumlem1  47145  ply1mulgsumlem2  47146  lincsumcl  47190  lincscmcl  47191  ellcoellss  47194  sepfsepc  47638  seppcld  47640