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  3590  rexopabb  5477  unon  7776  tfrlem16  8326  oawordeulem  8483  nneob  8586  unfi  9099  ominf  9168  unfilem1  9209  fival  9319  elfi2  9321  fi0  9327  fiin  9329  djuss  9838  djuun  9844  updjud  9852  finnum  9866  dif1card  9926  fseqenlem2  9941  dfac8alem  9945  alephfp  10024  cflim2  10179  isfin1-3  10302  fin67  10311  isfin7-2  10312  axdc3lem  10366  axdc3lem2  10367  iunfo  10455  iundom2g  10456  winainflem  10610  rankcf  10694  map2psrpr  11027  supsrlem  11028  1re  11138  0re  11140  00id  11315  addrid  11320  0cnALT  11375  om2uzrani  13908  uzrdgfni  13914  wrdf  14474  rexanuz  15302  r19.2uz  15308  fsum2dlem  15726  fsumcom2  15730  fprod2dlem  15939  fprodcom2  15943  0dvds  16239  even2n  16305  m1expe  16337  m1exp1  16339  modprm0  16770  cshwsidrepsw  17058  smndex1basss  18870  smndex1mgm  18872  smndex1mndlem  18874  dfgrp2  18932  pzriprnglem4  21477  psgndiflemA  21594  ppttop  22985  epttop  22987  neips  23091  lmmo  23358  2ndctop  23425  2ndcsep  23437  fbncp  23817  fgcl  23856  filuni  23863  tgioo  24774  zcld  24792  cphsscph  25231  elovolm  25455  nulmbl2  25516  ellimc3  25859  limcflf  25861  pilem3  26434  perfect  27211  2vmadivsum  27521  selberg3lem2  27538  selberg4  27541  pntrsumbnd2  27547  pntrlog2bndlem3  27559  pntrlog2bndlem4  27560  pntpbnd  27568  pnt3  27592  elnoOLD  27627  noreson  27641  nosupbnd1lem5  27693  noinfbnd1lem5  27708  axcontlem12  29061  axcont  29062  clwwlkn1loopb  30131  eleclclwwlkn  30164  uhgr3cyclex  30270  frgrreggt1  30481  norm1exi  31339  nmcexi  32115  lnconi  32122  pjssdif1i  32264  stri  32346  hstri  32354  stcltrthi  32367  shatomici  32447  qsxpid  33440  dispcmp  34022  isrnmeas  34363  dya2iocucvr  34447  sxbrsigalem1  34448  eulerpartlemt  34534  bnj1398  35195  bnj1498  35222  fnrelpredd  35253  r1omfi  35267  wevgblacfn  35310  satfrnmapom  35571  gonar  35596  goalr  35598  satffun  35610  mthmblem  35781  lindsdom  37952  mblfinlem3  37997  ismblfin  37999  volsupnfl  38003  itg2addnclem  38009  itg2addnc  38012  cover2  38053  prtlem16  39332  rexzrexnn0  43253  isnumbasgrplem2  43553  dgraalem  43594  onsucrn  43720  dflim5  43778  dfno2  43876  rp-isfinite5  43965  mnurndlem1  44729  grumnudlem  44733  gruex  44746  islptre  46070  stirlinglem13  46535  stirlinglem14  46536  stirling  46538  etransc  46732  ovolval4lem2  47099  sprsymrelf1lem  47966  sprsymrelfolem2  47968  prmdvdsfmtnof  48064  prmdvdsfmtnof1  48065  perfectALTV  48214  tgoldbach  48308  uspgrsprf  48637  2zlidl  48731  2zrngamgm  48736  ply1mulgsumlem1  48877  ply1mulgsumlem2  48878  lincsumcl  48922  lincscmcl  48923  ellcoellss  48926  sepfsepc  49418  seppcld  49420