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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1781   ∈ wcel 2114  ∃wrex 3062

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 1912

This theorem depends on definitions:  df-bi 207  df-ex 1782  df-rex 3063

This theorem is referenced by:  rexlimiv  3132  rexlimivw  3135  rexraleqim  3603  rexopabb  5484  unon  7783  tfrlem16  8334  oawordeulem  8491  nneob  8594  unfi  9107  ominf  9176  unfilem1  9217  fival  9327  elfi2  9329  fi0  9335  fiin  9337  djuss  9844  djuun  9850  updjud  9858  finnum  9872  dif1card  9932  fseqenlem2  9947  dfac8alem  9951  alephfp  10030  cflim2  10185  isfin1-3  10308  fin67  10317  isfin7-2  10318  axdc3lem  10372  axdc3lem2  10373  iunfo  10461  iundom2g  10462  winainflem  10616  rankcf  10700  map2psrpr  11033  supsrlem  11034  1re  11144  0re  11146  00id  11320  addrid  11325  0cnALT  11380  om2uzrani  13887  uzrdgfni  13893  wrdf  14453  rexanuz  15281  r19.2uz  15287  fsum2dlem  15705  fsumcom2  15709  fprod2dlem  15915  fprodcom2  15919  0dvds  16215  even2n  16281  m1expe  16313  m1exp1  16315  modprm0  16745  cshwsidrepsw  17033  smndex1basss  18842  smndex1mgm  18844  smndex1mndlem  18846  dfgrp2  18904  pzriprnglem4  21451  psgndiflemA  21568  ppttop  22963  epttop  22965  neips  23069  lmmo  23336  2ndctop  23403  2ndcsep  23415  fbncp  23795  fgcl  23834  filuni  23841  tgioo  24752  zcld  24770  cphsscph  25219  elovolm  25444  nulmbl2  25505  ellimc3  25848  limcflf  25850  pilem3  26431  perfect  27210  2vmadivsum  27520  selberg3lem2  27537  selberg4  27540  pntrsumbnd2  27546  pntrlog2bndlem3  27558  pntrlog2bndlem4  27559  pntpbnd  27567  pnt3  27591  elnoOLD  27626  noreson  27640  nosupbnd1lem5  27692  noinfbnd1lem5  27707  axcontlem12  29060  axcont  29061  clwwlkn1loopb  30130  eleclclwwlkn  30163  uhgr3cyclex  30269  frgrreggt1  30480  norm1exi  31338  nmcexi  32114  lnconi  32121  pjssdif1i  32263  stri  32345  hstri  32353  stcltrthi  32366  shatomici  32446  qsxpid  33455  dispcmp  34037  isrnmeas  34378  dya2iocucvr  34462  sxbrsigalem1  34463  eulerpartlemt  34549  bnj1398  35210  bnj1498  35237  fnrelpredd  35268  r1omfi  35282  wevgblacfn  35325  satfrnmapom  35586  gonar  35611  goalr  35613  satffun  35625  mthmblem  35796  lindsdom  37865  mblfinlem3  37910  ismblfin  37912  volsupnfl  37916  itg2addnclem  37922  itg2addnc  37925  cover2  37966  prtlem16  39245  rexzrexnn0  43161  isnumbasgrplem2  43461  dgraalem  43502  onsucrn  43628  dflim5  43686  dfno2  43784  rp-isfinite5  43873  mnurndlem1  44637  grumnudlem  44641  gruex  44654  islptre  45979  stirlinglem13  46444  stirlinglem14  46445  stirling  46447  etransc  46641  ovolval4lem2  47008  sprsymrelf1lem  47851  sprsymrelfolem2  47853  prmdvdsfmtnof  47946  prmdvdsfmtnof1  47947  perfectALTV  48083  tgoldbach  48177  uspgrsprf  48506  2zlidl  48600  2zrngamgm  48605  ply1mulgsumlem1  48746  ply1mulgsumlem2  48747  lincsumcl  48791  lincscmcl  48792  ellcoellss  48795  sepfsepc  49287  seppcld  49289