Theorem rexlimiva 3133

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1779   ∈ wcel 2108  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-rex 3061

This theorem is referenced by:  rexlimiv  3134  rexlimivw  3137  rexraleqim  3626  rexopabb  5503  unon  7825  tfrlem16  8407  oawordeulem  8566  nneob  8668  unfi  9185  ominf  9266  ominfOLD  9267  unfilem1  9315  fival  9424  elfi2  9426  fi0  9432  fiin  9434  djuss  9934  djuun  9940  updjud  9948  finnum  9962  dif1card  10024  fseqenlem2  10039  dfac8alem  10043  alephfp  10122  cflim2  10277  isfin1-3  10400  fin67  10409  isfin7-2  10410  axdc3lem  10464  axdc3lem2  10465  iunfo  10553  iundom2g  10554  winainflem  10707  rankcf  10791  map2psrpr  11124  supsrlem  11125  1re  11235  0re  11237  00id  11410  addrid  11415  0cnALT  11470  om2uzrani  13970  uzrdgfni  13976  wrdf  14536  rexanuz  15364  r19.2uz  15370  fsum2dlem  15786  fsumcom2  15790  fprod2dlem  15996  fprodcom2  16000  0dvds  16296  even2n  16361  m1expe  16393  m1exp1  16395  modprm0  16825  cshwsidrepsw  17113  smndex1basss  18883  smndex1mgm  18885  smndex1mndlem  18887  dfgrp2  18945  pzriprnglem4  21445  psgndiflemA  21561  ppttop  22945  epttop  22947  neips  23051  lmmo  23318  2ndctop  23385  2ndcsep  23397  fbncp  23777  fgcl  23816  filuni  23823  tgioo  24735  zcld  24753  cphsscph  25203  elovolm  25428  nulmbl2  25489  ellimc3  25832  limcflf  25834  pilem3  26415  perfect  27194  2vmadivsum  27504  selberg3lem2  27521  selberg4  27524  pntrsumbnd2  27530  pntrlog2bndlem3  27542  pntrlog2bndlem4  27543  pntpbnd  27551  pnt3  27575  elnoOLD  27610  noreson  27624  nosupbnd1lem5  27676  noinfbnd1lem5  27691  axcontlem12  28954  axcont  28955  clwwlkn1loopb  30024  eleclclwwlkn  30057  uhgr3cyclex  30163  frgrreggt1  30374  norm1exi  31231  nmcexi  32007  lnconi  32014  pjssdif1i  32156  stri  32238  hstri  32246  stcltrthi  32259  shatomici  32339  qsxpid  33377  dispcmp  33890  isrnmeas  34231  dya2iocucvr  34316  sxbrsigalem1  34317  eulerpartlemt  34403  bnj1398  35065  bnj1498  35092  fnrelpredd  35120  wevgblacfn  35131  satfrnmapom  35392  gonar  35417  goalr  35419  satffun  35431  mthmblem  35602  lindsdom  37638  mblfinlem3  37683  ismblfin  37685  volsupnfl  37689  itg2addnclem  37695  itg2addnc  37698  cover2  37739  prtlem16  38887  rexzrexnn0  42827  isnumbasgrplem2  43128  dgraalem  43169  onsucrn  43295  dflim5  43353  dfno2  43452  rp-isfinite5  43541  mnurndlem1  44305  grumnudlem  44309  gruex  44322  islptre  45648  stirlinglem13  46115  stirlinglem14  46116  stirling  46118  etransc  46312  ovolval4lem2  46679  sprsymrelf1lem  47505  sprsymrelfolem2  47507  prmdvdsfmtnof  47600  prmdvdsfmtnof1  47601  perfectALTV  47737  tgoldbach  47831  uspgrsprf  48121  2zlidl  48215  2zrngamgm  48220  ply1mulgsumlem1  48362  ply1mulgsumlem2  48363  lincsumcl  48407  lincscmcl  48408  ellcoellss  48411  sepfsepc  48902  seppcld  48904