Theorem rexlimiva 3155

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 3087	. 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 3086

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 3087

This theorem is used by:  rexlimiv  3156  rexlimivw  3159  rexraleqim  3601  rexopabb  5506  unon  7828  tfrlem16  8383  oawordeulem  8544  nneob  8647  unfi  9168  ominf  9237  unfilem1  9278  fival  9385  elfi2  9387  fi0  9393  fiin  9395  djuss  9928  djuun  9934  updjud  9942  finnum  9956  dif1card  10016  fseqenlem2  10031  dfac8alem  10035  alephfp  10114  cflim2  10268  isfin1-3  10391  fin67  10400  isfin7-2  10401  axdc3lem  10455  axdc3lem2  10456  iunfo  10550  iundom2g  10551  winainflem  10705  rankcf  10789  map2psrpr  11122  supsrlem  11123  1re  11235  0re  11237  00id  11412  addrid  11417  0cnALT  11472  om2uzrani  14019  uzrdgfni  14025  wrdf  14586  rexanuz  15436  r19.2uz  15442  fsum2dlem  15859  fsumcom2  15863  fprod2dlem  16070  fprodcom2  16074  0dvds  16369  even2n  16435  m1expe  16467  m1exp1  16469  modprm0  16900  cshwsidrepsw  17188  smndex1basss  19020  smndex1mgm  19022  smndex1mndlem  19024  dfgrp2  19089  qsxpid  19303  pzriprnglem4  21700  psgndiflemA  21817  lindsdom  22066  ppttop  23235  epttop  23237  neips  23341  lmmo  23608  2ndctop  23675  2ndcsep  23688  fbncp  24068  fgcl  24107  filuni  24114  tgioo  25025  zcld  25043  cphsscph  25482  elovolm  25706  nulmbl2  25767  ellimc3  26109  limcflf  26111  rnplynfin  26542  plyconz  26543  pilem3  26692  perfect  27470  2vmadivsum  27780  selberg3lem2  27797  selberg4  27800  pntrsumbnd2  27806  pntrlog2bndlem3  27818  pntrlog2bndlem4  27819  pntpbnd  27827  pnt3  27851  noreson  27899  nosupbnd1lem5  27951  noinfbnd1lem5  27966  axcontlem12  29435  axcont  29436  clwwlkn1loopb  30516  eleclclwwlkn  30549  uhgr3cyclex  30665  frgrreggt1  30876  norm1exi  31734  nmcexi  32510  lnconi  32517  pjssdif1i  32659  stri  32741  hstri  32749  stcltrthi  32762  shatomici  32842  dispcmp  34372  isrnmeas  34714  dya2iocucvr  34798  sxbrsigalem1  34799  eulerpartlemt  34885  bnj1398  35546  bnj1498  35573  fnrelpredd  35599  r1omfi  35616  wevgblacfn  35711  satfrnmapom  35952  gonar  35977  goalr  35979  satffun  35991  mthmblem  36162  mblfinlem3  38411  ismblfin  38413  volsupnfl  38417  itg2addnclem  38423  itg2addnc  38426  cover2  38468  prtlem16  39745  rexzrexnn0  43648  isnumbasgrplem2  43948  dgraalem  43989  onsucrn  44115  dflim5  44173  dfno2  44271  rp-isfinite5  44360  mnurndlem1  45108  grumnudlem  45112  gruex  45125  islptre  46452  stirlinglem13  46917  stirlinglem14  46918  stirling  46920  etransc  47114  ovolval4lem2  47481  sprsymrelf1lem  48394  sprsymrelfolem2  48396  prmdvdsfmtnof  48492  prmdvdsfmtnof1  48493  perfectALTV  48642  tgoldbach  48736  uspgrsprf  49065  2zlidl  49158  2zrngamgm  49163  ply1mulgsumlem1  49319  ply1mulgsumlem2  49320  lincsumcl  49364  lincscmcl  49365  ellcoellss  49368  sepfsepc  49857  seppcld  49859