Theorem rexlimiva 3160

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∃wex 1812   ∈ wcel 2146  ∃wrex 3091

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-ex 1813  df-rex 3092

This theorem is used by:  rexlimiv  3161  rexlimivw  3164  rexraleqim  3608  rexopabb  5514  unon  7833  tfrlem16  8386  oawordeulem  8545  nneob  8648  unfi  9162  ominf  9231  unfilem1  9272  fival  9379  elfi2  9381  fi0  9387  fiin  9389  djuss  9922  djuun  9928  updjud  9936  finnum  9950  dif1card  10010  fseqenlem2  10025  dfac8alem  10029  alephfp  10108  cflim2  10262  isfin1-3  10385  fin67  10394  isfin7-2  10395  axdc3lem  10449  axdc3lem2  10450  iunfo  10540  iundom2g  10541  winainflem  10695  rankcf  10779  map2psrpr  11112  supsrlem  11113  1re  11225  0re  11227  00id  11402  addrid  11407  0cnALT  11462  om2uzrani  14008  uzrdgfni  14014  wrdf  14575  rexanuz  15423  r19.2uz  15429  fsum2dlem  15846  fsumcom2  15850  fprod2dlem  16059  fprodcom2  16063  0dvds  16358  even2n  16424  m1expe  16456  m1exp1  16458  modprm0  16889  cshwsidrepsw  17177  smndex1basss  19006  smndex1mgm  19008  smndex1mndlem  19010  dfgrp2  19075  qsxpid  19289  pzriprnglem4  21686  psgndiflemA  21803  ppttop  23216  epttop  23218  neips  23322  lmmo  23589  2ndctop  23656  2ndcsep  23669  fbncp  24049  fgcl  24088  filuni  24095  tgioo  25006  zcld  25024  cphsscph  25463  elovolm  25687  nulmbl2  25748  ellimc3  26091  limcflf  26093  pilem3  26669  perfect  27448  2vmadivsum  27758  selberg3lem2  27775  selberg4  27778  pntrsumbnd2  27784  pntrlog2bndlem3  27796  pntrlog2bndlem4  27797  pntpbnd  27805  pnt3  27829  noreson  27877  nosupbnd1lem5  27929  noinfbnd1lem5  27944  axcontlem12  29382  axcont  29383  clwwlkn1loopb  30463  eleclclwwlkn  30496  uhgr3cyclex  30606  frgrreggt1  30817  norm1exi  31675  nmcexi  32451  lnconi  32458  pjssdif1i  32600  stri  32682  hstri  32690  stcltrthi  32703  shatomici  32783  dispcmp  34315  isrnmeas  34657  dya2iocucvr  34741  sxbrsigalem1  34742  eulerpartlemt  34828  bnj1398  35489  bnj1498  35516  fnrelpredd  35542  r1omfi  35559  wevgblacfn  35654  satfrnmapom  35901  gonar  35926  goalr  35928  satffun  35940  mthmblem  36111  lindsdom  38324  mblfinlem3  38369  ismblfin  38371  volsupnfl  38375  itg2addnclem  38381  itg2addnc  38384  cover2  38426  prtlem16  39703  rexzrexnn0  43591  isnumbasgrplem2  43891  dgraalem  43932  onsucrn  44058  dflim5  44116  dfno2  44214  rp-isfinite5  44303  mnurndlem1  45051  grumnudlem  45055  gruex  45068  islptre  46395  stirlinglem13  46860  stirlinglem14  46861  stirling  46863  etransc  47057  ovolval4lem2  47424  sprsymrelf1lem  48300  sprsymrelfolem2  48302  prmdvdsfmtnof  48398  prmdvdsfmtnof1  48399  perfectALTV  48548  tgoldbach  48642  uspgrsprf  48971  2zlidl  49064  2zrngamgm  49069  ply1mulgsumlem1  49225  ply1mulgsumlem2  49226  lincsumcl  49270  lincscmcl  49271  ellcoellss  49274  sepfsepc  49765  seppcld  49767