Theorem rexlimiva 3132

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

Syntax hints:   → wi 4   ∧ wa 396  ∃wex 1786   ∈ wcel 2119  ∃wrex 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-ex 1787  df-rex 3064

This theorem is referenced by:  rexlimiv  3133  rexlimivw  3136  rexraleqim  3585  rexopabb  5470  unon  7771  tfrlem16  8322  oawordeulem  8479  nneob  8582  unfi  9095  ominf  9164  unfilem1  9205  fival  9315  elfi2  9317  fi0  9323  fiin  9325  djuss  9835  djuun  9841  updjud  9849  finnum  9863  dif1card  9923  fseqenlem2  9938  dfac8alem  9942  alephfp  10021  cflim2  10176  isfin1-3  10299  fin67  10308  isfin7-2  10309  axdc3lem  10363  axdc3lem2  10364  iunfo  10452  iundom2g  10453  winainflem  10607  rankcf  10691  map2psrpr  11024  supsrlem  11025  1re  11135  0re  11137  00id  11312  addrid  11317  0cnALT  11372  om2uzrani  13905  uzrdgfni  13911  wrdf  14471  rexanuz  15299  r19.2uz  15305  fsum2dlem  15723  fsumcom2  15727  fprod2dlem  15936  fprodcom2  15940  0dvds  16236  even2n  16302  m1expe  16334  m1exp1  16336  modprm0  16767  cshwsidrepsw  17055  smndex1basss  18867  smndex1mgm  18869  smndex1mndlem  18871  dfgrp2  18929  pzriprnglem4  21459  psgndiflemA  21576  ppttop  22990  epttop  22992  neips  23096  lmmo  23363  2ndctop  23430  2ndcsep  23442  fbncp  23822  fgcl  23861  filuni  23868  tgioo  24779  zcld  24797  cphsscph  25236  elovolm  25460  nulmbl2  25521  ellimc3  25864  limcflf  25866  pilem3  26436  perfect  27212  2vmadivsum  27522  selberg3lem2  27539  selberg4  27542  pntrsumbnd2  27548  pntrlog2bndlem3  27560  pntrlog2bndlem4  27561  pntpbnd  27569  pnt3  27593  elnoOLD  27628  noreson  27642  nosupbnd1lem5  27694  noinfbnd1lem5  27709  axcontlem12  29062  axcont  29063  clwwlkn1loopb  30131  eleclclwwlkn  30164  uhgr3cyclex  30270  frgrreggt1  30481  norm1exi  31339  nmcexi  32115  lnconi  32122  pjssdif1i  32264  stri  32346  hstri  32354  stcltrthi  32367  shatomici  32447  qsxpid  33445  dispcmp  34043  isrnmeas  34384  dya2iocucvr  34468  sxbrsigalem1  34469  eulerpartlemt  34555  bnj1398  35216  bnj1498  35243  fnrelpredd  35272  r1omfi  35286  wevgblacfn  35337  satfrnmapom  35598  gonar  35623  goalr  35625  satffun  35637  mthmblem  35808  lindsdom  37981  mblfinlem3  38026  ismblfin  38028  volsupnfl  38032  itg2addnclem  38038  itg2addnc  38041  cover2  38082  prtlem16  39361  rexzrexnn0  43249  isnumbasgrplem2  43549  dgraalem  43590  onsucrn  43716  dflim5  43774  dfno2  43872  rp-isfinite5  43961  mnurndlem1  44725  grumnudlem  44729  gruex  44742  islptre  46064  stirlinglem13  46529  stirlinglem14  46530  stirling  46532  etransc  46726  ovolval4lem2  47093  sprsymrelf1lem  47966  sprsymrelfolem2  47968  prmdvdsfmtnof  48064  prmdvdsfmtnof1  48065  perfectALTV  48214  tgoldbach  48308  uspgrsprf  48637  2zlidl  48731  2zrngamgm  48736  ply1mulgsumlem1  48877  ply1mulgsumlem2  48878  lincsumcl  48922  lincscmcl  48923  ellcoellss  48926  sepfsepc  49418  seppcld  49420