Theorem rexlimiva 3126

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 3054	. 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 3053

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 3054

This theorem is referenced by:  rexlimiv  3127  rexlimivw  3130  rexraleqim  3613  rexopabb  5488  unon  7806  tfrlem16  8361  oawordeulem  8518  nneob  8620  unfi  9135  ominf  9205  ominfOLD  9206  unfilem1  9254  fival  9363  elfi2  9365  fi0  9371  fiin  9373  djuss  9873  djuun  9879  updjud  9887  finnum  9901  dif1card  9963  fseqenlem2  9978  dfac8alem  9982  alephfp  10061  cflim2  10216  isfin1-3  10339  fin67  10348  isfin7-2  10349  axdc3lem  10403  axdc3lem2  10404  iunfo  10492  iundom2g  10493  winainflem  10646  rankcf  10730  map2psrpr  11063  supsrlem  11064  1re  11174  0re  11176  00id  11349  addrid  11354  0cnALT  11409  om2uzrani  13917  uzrdgfni  13923  wrdf  14483  rexanuz  15312  r19.2uz  15318  fsum2dlem  15736  fsumcom2  15740  fprod2dlem  15946  fprodcom2  15950  0dvds  16246  even2n  16312  m1expe  16344  m1exp1  16346  modprm0  16776  cshwsidrepsw  17064  smndex1basss  18832  smndex1mgm  18834  smndex1mndlem  18836  dfgrp2  18894  pzriprnglem4  21394  psgndiflemA  21510  ppttop  22894  epttop  22896  neips  23000  lmmo  23267  2ndctop  23334  2ndcsep  23346  fbncp  23726  fgcl  23765  filuni  23772  tgioo  24684  zcld  24702  cphsscph  25151  elovolm  25376  nulmbl2  25437  ellimc3  25780  limcflf  25782  pilem3  26363  perfect  27142  2vmadivsum  27452  selberg3lem2  27469  selberg4  27472  pntrsumbnd2  27478  pntrlog2bndlem3  27490  pntrlog2bndlem4  27491  pntpbnd  27499  pnt3  27523  elnoOLD  27558  noreson  27572  nosupbnd1lem5  27624  noinfbnd1lem5  27639  axcontlem12  28902  axcont  28903  clwwlkn1loopb  29972  eleclclwwlkn  30005  uhgr3cyclex  30111  frgrreggt1  30322  norm1exi  31179  nmcexi  31955  lnconi  31962  pjssdif1i  32104  stri  32186  hstri  32194  stcltrthi  32207  shatomici  32287  qsxpid  33333  dispcmp  33849  isrnmeas  34190  dya2iocucvr  34275  sxbrsigalem1  34276  eulerpartlemt  34362  bnj1398  35024  bnj1498  35051  fnrelpredd  35079  wevgblacfn  35096  satfrnmapom  35357  gonar  35382  goalr  35384  satffun  35396  mthmblem  35567  lindsdom  37608  mblfinlem3  37653  ismblfin  37655  volsupnfl  37659  itg2addnclem  37665  itg2addnc  37668  cover2  37709  prtlem16  38862  rexzrexnn0  42792  isnumbasgrplem2  43093  dgraalem  43134  onsucrn  43260  dflim5  43318  dfno2  43417  rp-isfinite5  43506  mnurndlem1  44270  grumnudlem  44274  gruex  44287  islptre  45617  stirlinglem13  46084  stirlinglem14  46085  stirling  46087  etransc  46281  ovolval4lem2  46648  sprsymrelf1lem  47492  sprsymrelfolem2  47494  prmdvdsfmtnof  47587  prmdvdsfmtnof1  47588  perfectALTV  47724  tgoldbach  47818  uspgrsprf  48134  2zlidl  48228  2zrngamgm  48233  ply1mulgsumlem1  48375  ply1mulgsumlem2  48376  lincsumcl  48420  lincscmcl  48421  ellcoellss  48424  sepfsepc  48916  seppcld  48918