Theorem rexlimiva 3127

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1779   ∈ wcel 2109  ∃wrex 3054

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-rex 3055

This theorem is referenced by:  rexlimiv  3128  rexlimivw  3131  rexraleqim  3616  rexopabb  5491  unon  7809  tfrlem16  8364  oawordeulem  8521  nneob  8623  unfi  9141  ominf  9212  ominfOLD  9213  unfilem1  9261  fival  9370  elfi2  9372  fi0  9378  fiin  9380  djuss  9880  djuun  9886  updjud  9894  finnum  9908  dif1card  9970  fseqenlem2  9985  dfac8alem  9989  alephfp  10068  cflim2  10223  isfin1-3  10346  fin67  10355  isfin7-2  10356  axdc3lem  10410  axdc3lem2  10411  iunfo  10499  iundom2g  10500  winainflem  10653  rankcf  10737  map2psrpr  11070  supsrlem  11071  1re  11181  0re  11183  00id  11356  addrid  11361  0cnALT  11416  om2uzrani  13924  uzrdgfni  13930  wrdf  14490  rexanuz  15319  r19.2uz  15325  fsum2dlem  15743  fsumcom2  15747  fprod2dlem  15953  fprodcom2  15957  0dvds  16253  even2n  16319  m1expe  16351  m1exp1  16353  modprm0  16783  cshwsidrepsw  17071  smndex1basss  18839  smndex1mgm  18841  smndex1mndlem  18843  dfgrp2  18901  pzriprnglem4  21401  psgndiflemA  21517  ppttop  22901  epttop  22903  neips  23007  lmmo  23274  2ndctop  23341  2ndcsep  23353  fbncp  23733  fgcl  23772  filuni  23779  tgioo  24691  zcld  24709  cphsscph  25158  elovolm  25383  nulmbl2  25444  ellimc3  25787  limcflf  25789  pilem3  26370  perfect  27149  2vmadivsum  27459  selberg3lem2  27476  selberg4  27479  pntrsumbnd2  27485  pntrlog2bndlem3  27497  pntrlog2bndlem4  27498  pntpbnd  27506  pnt3  27530  elnoOLD  27565  noreson  27579  nosupbnd1lem5  27631  noinfbnd1lem5  27646  axcontlem12  28909  axcont  28910  clwwlkn1loopb  29979  eleclclwwlkn  30012  uhgr3cyclex  30118  frgrreggt1  30329  norm1exi  31186  nmcexi  31962  lnconi  31969  pjssdif1i  32111  stri  32193  hstri  32201  stcltrthi  32214  shatomici  32294  qsxpid  33340  dispcmp  33856  isrnmeas  34197  dya2iocucvr  34282  sxbrsigalem1  34283  eulerpartlemt  34369  bnj1398  35031  bnj1498  35058  fnrelpredd  35086  wevgblacfn  35103  satfrnmapom  35364  gonar  35389  goalr  35391  satffun  35403  mthmblem  35574  lindsdom  37615  mblfinlem3  37660  ismblfin  37662  volsupnfl  37666  itg2addnclem  37672  itg2addnc  37675  cover2  37716  prtlem16  38869  rexzrexnn0  42799  isnumbasgrplem2  43100  dgraalem  43141  onsucrn  43267  dflim5  43325  dfno2  43424  rp-isfinite5  43513  mnurndlem1  44277  grumnudlem  44281  gruex  44294  islptre  45624  stirlinglem13  46091  stirlinglem14  46092  stirling  46094  etransc  46288  ovolval4lem2  46655  sprsymrelf1lem  47496  sprsymrelfolem2  47498  prmdvdsfmtnof  47591  prmdvdsfmtnof1  47592  perfectALTV  47728  tgoldbach  47822  uspgrsprf  48138  2zlidl  48232  2zrngamgm  48237  ply1mulgsumlem1  48379  ply1mulgsumlem2  48380  lincsumcl  48424  lincscmcl  48425  ellcoellss  48428  sepfsepc  48920  seppcld  48922