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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1780   ∈ wcel 2113  ∃wrex 3058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-ex 1781  df-rex 3059

This theorem is referenced by:  rexlimiv  3128  rexlimivw  3131  rexraleqim  3599  rexopabb  5474  unon  7771  tfrlem16  8322  oawordeulem  8479  nneob  8582  unfi  9093  ominf  9162  unfilem1  9203  fival  9313  elfi2  9315  fi0  9321  fiin  9323  djuss  9830  djuun  9836  updjud  9844  finnum  9858  dif1card  9918  fseqenlem2  9933  dfac8alem  9937  alephfp  10016  cflim2  10171  isfin1-3  10294  fin67  10303  isfin7-2  10304  axdc3lem  10358  axdc3lem2  10359  iunfo  10447  iundom2g  10448  winainflem  10602  rankcf  10686  map2psrpr  11019  supsrlem  11020  1re  11130  0re  11132  00id  11306  addrid  11311  0cnALT  11366  om2uzrani  13873  uzrdgfni  13879  wrdf  14439  rexanuz  15267  r19.2uz  15273  fsum2dlem  15691  fsumcom2  15695  fprod2dlem  15901  fprodcom2  15905  0dvds  16201  even2n  16267  m1expe  16299  m1exp1  16301  modprm0  16731  cshwsidrepsw  17019  smndex1basss  18828  smndex1mgm  18830  smndex1mndlem  18832  dfgrp2  18890  pzriprnglem4  21437  psgndiflemA  21554  ppttop  22949  epttop  22951  neips  23055  lmmo  23322  2ndctop  23389  2ndcsep  23401  fbncp  23781  fgcl  23820  filuni  23827  tgioo  24738  zcld  24756  cphsscph  25205  elovolm  25430  nulmbl2  25491  ellimc3  25834  limcflf  25836  pilem3  26417  perfect  27196  2vmadivsum  27506  selberg3lem2  27523  selberg4  27526  pntrsumbnd2  27532  pntrlog2bndlem3  27544  pntrlog2bndlem4  27545  pntpbnd  27553  pnt3  27577  elnoOLD  27612  noreson  27626  nosupbnd1lem5  27678  noinfbnd1lem5  27693  axcontlem12  28997  axcont  28998  clwwlkn1loopb  30067  eleclclwwlkn  30100  uhgr3cyclex  30206  frgrreggt1  30417  norm1exi  31274  nmcexi  32050  lnconi  32057  pjssdif1i  32199  stri  32281  hstri  32289  stcltrthi  32302  shatomici  32382  qsxpid  33392  dispcmp  33965  isrnmeas  34306  dya2iocucvr  34390  sxbrsigalem1  34391  eulerpartlemt  34477  bnj1398  35139  bnj1498  35166  fnrelpredd  35196  r1omfi  35210  wevgblacfn  35252  satfrnmapom  35513  gonar  35538  goalr  35540  satffun  35552  mthmblem  35723  lindsdom  37754  mblfinlem3  37799  ismblfin  37801  volsupnfl  37805  itg2addnclem  37811  itg2addnc  37814  cover2  37855  prtlem16  39068  rexzrexnn0  42988  isnumbasgrplem2  43288  dgraalem  43329  onsucrn  43455  dflim5  43513  dfno2  43611  rp-isfinite5  43700  mnurndlem1  44464  grumnudlem  44468  gruex  44481  islptre  45807  stirlinglem13  46272  stirlinglem14  46273  stirling  46275  etransc  46469  ovolval4lem2  46836  sprsymrelf1lem  47679  sprsymrelfolem2  47681  prmdvdsfmtnof  47774  prmdvdsfmtnof1  47775  perfectALTV  47911  tgoldbach  48005  uspgrsprf  48334  2zlidl  48428  2zrngamgm  48433  ply1mulgsumlem1  48574  ply1mulgsumlem2  48575  lincsumcl  48619  lincscmcl  48620  ellcoellss  48623  sepfsepc  49115  seppcld  49117