Theorem rexlimiva 3153

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1777   ∈ wcel 2108  ∃wrex 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-ex 1778  df-rex 3077

This theorem is referenced by:  rexlimiv  3154  rexlimivw  3157  rexraleqim  3660  rexopabb  5547  unon  7867  tfrlem16  8449  oawordeulem  8610  nneob  8712  unfi  9238  ominf  9321  ominfOLD  9322  unfilem1  9371  pwfiOLD  9417  fival  9481  elfi2  9483  fi0  9489  fiin  9491  djuss  9989  djuun  9995  updjud  10003  finnum  10017  dif1card  10079  fseqenlem2  10094  dfac8alem  10098  alephfp  10177  cflim2  10332  isfin1-3  10455  fin67  10464  isfin7-2  10465  axdc3lem  10519  axdc3lem2  10520  iunfo  10608  iundom2g  10609  winainflem  10762  rankcf  10846  map2psrpr  11179  supsrlem  11180  1re  11290  0re  11292  00id  11465  addrid  11470  0cnALT  11524  om2uzrani  14003  uzrdgfni  14009  wrdf  14567  rexanuz  15394  r19.2uz  15400  fsum2dlem  15818  fsumcom2  15822  fprod2dlem  16028  fprodcom2  16032  0dvds  16325  even2n  16390  m1expe  16422  m1exp1  16424  modprm0  16852  cshwsidrepsw  17141  smndex1basss  18940  smndex1mgm  18942  smndex1mndlem  18944  dfgrp2  19002  pzriprnglem4  21518  psgndiflemA  21642  ppttop  23035  epttop  23037  neips  23142  lmmo  23409  2ndctop  23476  2ndcsep  23488  fbncp  23868  fgcl  23907  filuni  23914  tgioo  24837  zcld  24854  cphsscph  25304  elovolm  25529  nulmbl2  25590  ellimc3  25934  limcflf  25936  pilem3  26515  perfect  27293  2vmadivsum  27603  selberg3lem2  27620  selberg4  27623  pntrsumbnd2  27629  pntrlog2bndlem3  27641  pntrlog2bndlem4  27642  pntpbnd  27650  pnt3  27674  elnoOLD  27709  noreson  27723  nosupbnd1lem5  27775  noinfbnd1lem5  27790  axcontlem12  29008  axcont  29009  clwwlkn1loopb  30075  eleclclwwlkn  30108  uhgr3cyclex  30214  frgrreggt1  30425  norm1exi  31282  nmcexi  32058  lnconi  32065  pjssdif1i  32207  stri  32289  hstri  32297  stcltrthi  32310  shatomici  32390  qsxpid  33355  dispcmp  33805  isrnmeas  34164  dya2iocucvr  34249  sxbrsigalem1  34250  eulerpartlemt  34336  bnj1398  35010  bnj1498  35037  fnrelpredd  35065  wevgblacfn  35076  satfrnmapom  35338  gonar  35363  goalr  35365  satffun  35377  mthmblem  35548  lindsdom  37574  mblfinlem3  37619  ismblfin  37621  volsupnfl  37625  itg2addnclem  37631  itg2addnc  37634  cover2  37675  prtlem16  38825  rexzrexnn0  42760  isnumbasgrplem2  43061  dgraalem  43102  onsucrn  43233  dflim5  43291  dfno2  43390  rp-isfinite5  43479  mnurndlem1  44250  grumnudlem  44254  gruex  44267  islptre  45540  stirlinglem13  46007  stirlinglem14  46008  stirling  46010  etransc  46204  ovolval4lem2  46571  sprsymrelf1lem  47365  sprsymrelfolem2  47367  prmdvdsfmtnof  47460  prmdvdsfmtnof1  47461  perfectALTV  47597  tgoldbach  47691  uspgrsprf  47869  2zlidl  47963  2zrngamgm  47968  ply1mulgsumlem1  48115  ply1mulgsumlem2  48116  lincsumcl  48160  lincscmcl  48161  ellcoellss  48164  sepfsepc  48607  seppcld  48609