Theorem rexlimiva 3164

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

Syntax hints:   → wi 4   ∧ wa 400  ∃wex 1806   ∈ wcel 2149  ∃wrex 3095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-ex 1807  df-rex 3096

This theorem is referenced by:  rexlimiv  3165  rexlimivw  3168  rexraleqim  3615  rexopabb  5513  unon  7827  tfrlem16  8380  oawordeulem  8539  nneob  8642  unfi  9155  ominf  9224  unfilem1  9265  fival  9372  elfi2  9374  fi0  9380  fiin  9382  djuss  9906  djuun  9912  updjud  9920  finnum  9934  dif1card  9994  fseqenlem2  10009  dfac8alem  10013  alephfp  10092  cflim2  10247  isfin1-3  10370  fin67  10379  isfin7-2  10380  axdc3lem  10434  axdc3lem2  10435  iunfo  10523  iundom2g  10524  winainflem  10678  rankcf  10762  map2psrpr  11095  supsrlem  11096  1re  11208  0re  11210  00id  11385  addrid  11390  0cnALT  11445  om2uzrani  13988  uzrdgfni  13994  wrdf  14555  rexanuz  15397  r19.2uz  15403  fsum2dlem  15821  fsumcom2  15825  fprod2dlem  16034  fprodcom2  16038  0dvds  16334  even2n  16400  m1expe  16432  m1exp1  16434  modprm0  16865  cshwsidrepsw  17153  smndex1basss  18967  smndex1mgm  18969  smndex1mndlem  18971  dfgrp2  19029  qsxpid  19243  pzriprnglem4  21603  psgndiflemA  21720  ppttop  23133  epttop  23135  neips  23239  lmmo  23506  2ndctop  23573  2ndcsep  23585  fbncp  23965  fgcl  24004  filuni  24011  tgioo  24922  zcld  24940  cphsscph  25379  elovolm  25603  nulmbl2  25664  ellimc3  26007  limcflf  26009  pilem3  26582  perfect  27361  2vmadivsum  27671  selberg3lem2  27688  selberg4  27691  pntrsumbnd2  27697  pntrlog2bndlem3  27709  pntrlog2bndlem4  27710  pntpbnd  27718  pnt3  27742  noreson  27790  nosupbnd1lem5  27842  noinfbnd1lem5  27857  axcontlem12  29266  axcont  29267  clwwlkn1loopb  30335  eleclclwwlkn  30368  uhgr3cyclex  30474  frgrreggt1  30685  norm1exi  31543  nmcexi  32319  lnconi  32326  pjssdif1i  32468  stri  32550  hstri  32558  stcltrthi  32571  shatomici  32651  dispcmp  34194  isrnmeas  34535  dya2iocucvr  34619  sxbrsigalem1  34620  eulerpartlemt  34706  bnj1398  35367  bnj1498  35394  fnrelpredd  35425  r1omfi  35441  wevgblacfn  35494  satfrnmapom  35761  gonar  35786  goalr  35788  satffun  35800  mthmblem  35971  lindsdom  38153  mblfinlem3  38198  ismblfin  38200  volsupnfl  38204  itg2addnclem  38210  itg2addnc  38213  cover2  38254  prtlem16  39533  rexzrexnn0  43423  isnumbasgrplem2  43723  dgraalem  43764  onsucrn  43890  dflim5  43948  dfno2  44046  rp-isfinite5  44135  mnurndlem1  44883  grumnudlem  44887  gruex  44900  islptre  46227  stirlinglem13  46692  stirlinglem14  46693  stirling  46695  etransc  46889  ovolval4lem2  47256  sprsymrelf1lem  48129  sprsymrelfolem2  48131  prmdvdsfmtnof  48227  prmdvdsfmtnof1  48228  perfectALTV  48377  tgoldbach  48471  uspgrsprf  48800  2zlidl  48894  2zrngamgm  48899  ply1mulgsumlem1  49051  ply1mulgsumlem2  49052  lincsumcl  49096  lincscmcl  49097  ellcoellss  49100  sepfsepc  49591  seppcld  49593