Theorem rexlimiva 3158

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

Syntax hints:   → wi 4   ∧ wa 400  ∃wex 1809   ∈ wcel 2143  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

This theorem depends on definitions:  df-bi 210  df-ex 1810  df-rex 3090

This theorem is referenced by:  rexlimiv  3159  rexlimivw  3162  rexraleqim  3606  rexopabb  5512  unon  7823  tfrlem16  8376  oawordeulem  8535  nneob  8638  unfi  9151  ominf  9220  unfilem1  9261  fival  9368  elfi2  9370  fi0  9376  fiin  9378  djuss  9902  djuun  9908  updjud  9916  finnum  9930  dif1card  9990  fseqenlem2  10005  dfac8alem  10009  alephfp  10088  cflim2  10242  isfin1-3  10365  fin67  10374  isfin7-2  10375  axdc3lem  10429  axdc3lem2  10430  iunfo  10518  iundom2g  10519  winainflem  10673  rankcf  10757  map2psrpr  11090  supsrlem  11091  1re  11203  0re  11205  00id  11380  addrid  11385  0cnALT  11440  om2uzrani  13984  uzrdgfni  13990  wrdf  14551  rexanuz  15393  r19.2uz  15399  fsum2dlem  15817  fsumcom2  15821  fprod2dlem  16030  fprodcom2  16034  0dvds  16329  even2n  16395  m1expe  16427  m1exp1  16429  modprm0  16860  cshwsidrepsw  17148  smndex1basss  18962  smndex1mgm  18964  smndex1mndlem  18966  dfgrp2  19024  qsxpid  19238  pzriprnglem4  21634  psgndiflemA  21751  ppttop  23164  epttop  23166  neips  23270  lmmo  23537  2ndctop  23604  2ndcsep  23616  fbncp  23996  fgcl  24035  filuni  24042  tgioo  24953  zcld  24971  cphsscph  25410  elovolm  25634  nulmbl2  25695  ellimc3  26038  limcflf  26040  pilem3  26616  perfect  27395  2vmadivsum  27705  selberg3lem2  27722  selberg4  27725  pntrsumbnd2  27731  pntrlog2bndlem3  27743  pntrlog2bndlem4  27744  pntpbnd  27752  pnt3  27776  noreson  27824  nosupbnd1lem5  27876  noinfbnd1lem5  27891  axcontlem12  29325  axcont  29326  clwwlkn1loopb  30394  eleclclwwlkn  30427  uhgr3cyclex  30533  frgrreggt1  30744  norm1exi  31602  nmcexi  32378  lnconi  32385  pjssdif1i  32527  stri  32609  hstri  32617  stcltrthi  32630  shatomici  32710  dispcmp  34249  isrnmeas  34590  dya2iocucvr  34674  sxbrsigalem1  34675  eulerpartlemt  34761  bnj1398  35422  bnj1498  35449  fnrelpredd  35482  r1omfi  35499  wevgblacfn  35595  satfrnmapom  35862  gonar  35887  goalr  35889  satffun  35901  mthmblem  36072  lindsdom  38285  mblfinlem3  38330  ismblfin  38332  volsupnfl  38336  itg2addnclem  38342  itg2addnc  38345  cover2  38386  prtlem16  39663  rexzrexnn0  43551  isnumbasgrplem2  43851  dgraalem  43892  onsucrn  44018  dflim5  44076  dfno2  44174  rp-isfinite5  44263  mnurndlem1  45011  grumnudlem  45015  gruex  45028  islptre  46355  stirlinglem13  46820  stirlinglem14  46821  stirling  46823  etransc  47017  ovolval4lem2  47384  sprsymrelf1lem  48260  sprsymrelfolem2  48262  prmdvdsfmtnof  48358  prmdvdsfmtnof1  48359  perfectALTV  48508  tgoldbach  48602  uspgrsprf  48931  2zlidl  49025  2zrngamgm  49030  ply1mulgsumlem1  49186  ply1mulgsumlem2  49187  lincsumcl  49231  lincscmcl  49232  ellcoellss  49235  sepfsepc  49726  seppcld  49728