Theorem rexlimiva 3156

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 3088	. 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 2145  ∃wrex 3087

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 3088

This theorem is used by:  rexlimiv  3157  rexlimivw  3160  rexraleqim  3601  rexopabb  5502  unon  7842  tfrlem16  8401  oawordeulem  8562  nneob  8665  unfi  9186  ominf  9255  unfilem1  9297  fival  9404  elfi2  9406  fi0  9412  fiin  9414  hffi  9909  djuss  10001  djuun  10007  updjud  10015  finnum  10029  dif1card  10089  fseqenlem2  10104  dfac8alem  10108  alephfp  10187  cflim2  10341  isfin1-3  10464  fin67  10473  isfin7-2  10474  axdc3lem  10528  axdc3lem2  10529  iunfo  10623  iundom2g  10624  winainflem  10778  rankcf  10862  map2psrpr  11195  supsrlem  11196  1re  11308  0re  11310  00id  11485  addrid  11490  0cnALT  11545  om2uzrani  14095  uzrdgfni  14101  wrdf  14663  rexanuz  15513  r19.2uz  15519  fsum2dlem  15936  fsumcom2  15940  fprod2dlem  16147  fprodcom2  16151  0dvds  16446  even2n  16512  m1expe  16544  m1exp1  16546  modprm0  16983  cshwsidrepsw  17271  smndex1basss  19104  smndex1mgm  19106  smndex1mndlem  19108  dfgrp2  19173  qsxpid  19387  pzriprnglem4  21790  psgndiflemA  21907  lindsdom  22156  ppttop  23325  epttop  23327  neips  23431  lmmo  23698  2ndctop  23765  2ndcsep  23778  fbncp  24158  fgcl  24197  filuni  24204  tgioo  25115  zcld  25133  cphsscph  25572  elovolm  25796  nulmbl2  25857  ellimc3  26199  limcflf  26201  rnplynfin  26630  plyconz  26631  pilem3  26780  perfect  27558  2vmadivsum  27868  selberg3lem2  27885  selberg4  27888  pntrsumbnd2  27894  pntrlog2bndlem3  27906  pntrlog2bndlem4  27907  pntpbnd  27915  pnt3  27939  noreson  28017  nosupbnd1lem5  28069  noinfbnd1lem5  28084  axcontlem12  29553  axcont  29554  clwwlkn1loopb  30634  eleclclwwlkn  30667  uhgr3cyclex  30783  frgrreggt1  30994  norm1exi  31852  nmcexi  32628  lnconi  32635  pjssdif1i  32777  stri  32859  hstri  32867  stcltrthi  32880  shatomici  32960  dispcmp  34491  isrnmeas  34833  dya2iocucvr  34916  sxbrsigalem1  34917  eulerpartlemt  35003  bnj1398  35664  bnj1498  35691  fnrelpredd  35720  acwer1prc  35760  wevgblacfn  35890  satfrnmapom  36135  gonar  36160  goalr  36162  satffun  36174  mthmblem  36345  mblfinlem3  38577  ismblfin  38579  volsupnfl  38583  itg2addnclem  38589  itg2addnc  38592  dfprop1  38645  cover2  38649  prtlem16  39926  rexzrexnn0  43810  isnumbasgrplem2  44105  dgraalem  44146  onsucrn  44272  dflim5  44330  dfno2  44428  rp-isfinite5  44517  mnurndlem1  45264  grumnudlem  45268  gruex  45281  islptre  46630  stirlinglem13  47095  stirlinglem14  47096  stirling  47098  etransc  47292  ovolval4lem2  47659  sprsymrelf1lem  48572  sprsymrelfolem2  48574  prmdvdsfmtnof  48670  prmdvdsfmtnof1  48671  perfectALTV  48820  tgoldbach  48914  uspgrsprf  49243  2zlidl  49336  2zrngamgm  49341  ply1mulgsumlem1  49497  ply1mulgsumlem2  49498  lincsumcl  49542  lincscmcl  49543  ellcoellss  49546  sepfsepc  50035  seppcld  50037