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  3610  rexopabb  5483  unon  7786  tfrlem16  8338  oawordeulem  8495  nneob  8597  unfi  9112  ominf  9181  ominfOLD  9182  unfilem1  9230  fival  9339  elfi2  9341  fi0  9347  fiin  9349  djuss  9849  djuun  9855  updjud  9863  finnum  9877  dif1card  9939  fseqenlem2  9954  dfac8alem  9958  alephfp  10037  cflim2  10192  isfin1-3  10315  fin67  10324  isfin7-2  10325  axdc3lem  10379  axdc3lem2  10380  iunfo  10468  iundom2g  10469  winainflem  10622  rankcf  10706  map2psrpr  11039  supsrlem  11040  1re  11150  0re  11152  00id  11325  addrid  11330  0cnALT  11385  om2uzrani  13893  uzrdgfni  13899  wrdf  14459  rexanuz  15288  r19.2uz  15294  fsum2dlem  15712  fsumcom2  15716  fprod2dlem  15922  fprodcom2  15926  0dvds  16222  even2n  16288  m1expe  16320  m1exp1  16322  modprm0  16752  cshwsidrepsw  17040  smndex1basss  18814  smndex1mgm  18816  smndex1mndlem  18818  dfgrp2  18876  pzriprnglem4  21426  psgndiflemA  21543  ppttop  22927  epttop  22929  neips  23033  lmmo  23300  2ndctop  23367  2ndcsep  23379  fbncp  23759  fgcl  23798  filuni  23805  tgioo  24717  zcld  24735  cphsscph  25184  elovolm  25409  nulmbl2  25470  ellimc3  25813  limcflf  25815  pilem3  26396  perfect  27175  2vmadivsum  27485  selberg3lem2  27502  selberg4  27505  pntrsumbnd2  27511  pntrlog2bndlem3  27523  pntrlog2bndlem4  27524  pntpbnd  27532  pnt3  27556  elnoOLD  27591  noreson  27605  nosupbnd1lem5  27657  noinfbnd1lem5  27672  axcontlem12  28955  axcont  28956  clwwlkn1loopb  30022  eleclclwwlkn  30055  uhgr3cyclex  30161  frgrreggt1  30372  norm1exi  31229  nmcexi  32005  lnconi  32012  pjssdif1i  32154  stri  32236  hstri  32244  stcltrthi  32257  shatomici  32337  qsxpid  33326  dispcmp  33842  isrnmeas  34183  dya2iocucvr  34268  sxbrsigalem1  34269  eulerpartlemt  34355  bnj1398  35017  bnj1498  35044  fnrelpredd  35072  wevgblacfn  35089  satfrnmapom  35350  gonar  35375  goalr  35377  satffun  35389  mthmblem  35560  lindsdom  37601  mblfinlem3  37646  ismblfin  37648  volsupnfl  37652  itg2addnclem  37658  itg2addnc  37661  cover2  37702  prtlem16  38855  rexzrexnn0  42785  isnumbasgrplem2  43086  dgraalem  43127  onsucrn  43253  dflim5  43311  dfno2  43410  rp-isfinite5  43499  mnurndlem1  44263  grumnudlem  44267  gruex  44280  islptre  45610  stirlinglem13  46077  stirlinglem14  46078  stirling  46080  etransc  46274  ovolval4lem2  46641  sprsymrelf1lem  47485  sprsymrelfolem2  47487  prmdvdsfmtnof  47580  prmdvdsfmtnof1  47581  perfectALTV  47717  tgoldbach  47811  uspgrsprf  48127  2zlidl  48221  2zrngamgm  48226  ply1mulgsumlem1  48368  ply1mulgsumlem2  48369  lincsumcl  48413  lincscmcl  48414  ellcoellss  48417  sepfsepc  48909  seppcld  48911