Theorem rexlimiva 3158

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∃wex 1811   ∈ wcel 2146  ∃wrex 3089

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944

This proof depends on definitions:  df-bi 210  df-ex 1812  df-rex 3090

This theorem is used by:  rexlimiv  3159  rexlimivw  3162  rexraleqim  3603  rexopabb  5505  unon  7849  tfrlem16  8412  oawordeulem  8573  nneob  8676  unfi  9197  ominf  9266  unfilem1  9308  fival  9414  elfi2  9416  fi0  9422  fiin  9424  hffi  9919  djuss  10011  djuun  10017  updjud  10025  finnum  10039  dif1card  10099  fseqenlem2  10114  dfac8alem  10118  alephfp  10197  cflim2  10351  isfin1-3  10474  fin67  10483  isfin7-2  10484  axdc3lem  10538  axdc3lem2  10539  iunfo  10633  iundom2g  10634  winainflem  10788  rankcf  10872  map2psrpr  11205  supsrlem  11206  1re  11318  0re  11320  00id  11495  addrid  11500  0cnALT  11555  om2uzrani  14105  uzrdgfni  14111  wrdf  14673  rexanuz  15525  r19.2uz  15531  fsum2dlem  15948  fsumcom2  15952  fprod2dlem  16159  fprodcom2  16163  0dvds  16458  even2n  16524  m1expe  16556  m1exp1  16558  modprm0  16995  cshwsidrepsw  17283  smndex1basss  19116  smndex1mgm  19118  smndex1mndlem  19120  dfgrp2  19185  qsxpid  19399  pzriprnglem4  21802  psgndiflemA  21919  lindsdom  22168  ppttop  23337  epttop  23339  neips  23443  lmmo  23710  2ndctop  23777  2ndcsep  23790  fbncp  24170  fgcl  24209  filuni  24216  tgioo  25127  zcld  25145  cphsscph  25584  elovolm  25808  nulmbl2  25869  ellimc3  26211  limcflf  26213  rnplynfin  26642  plyconz  26643  pilem3  26792  perfect  27570  2vmadivsum  27880  selberg3lem2  27897  selberg4  27900  pntrsumbnd2  27906  pntrlog2bndlem3  27918  pntrlog2bndlem4  27919  pntpbnd  27927  pnt3  27951  noreson  28029  nosupbnd1lem5  28081  noinfbnd1lem5  28096  axcontlem12  29565  axcont  29566  clwwlkn1loopb  30646  eleclclwwlkn  30679  uhgr3cyclex  30795  frgrreggt1  31006  norm1exi  31864  nmcexi  32640  lnconi  32647  pjssdif1i  32789  stri  32871  hstri  32879  stcltrthi  32892  shatomici  32972  dispcmp  34544  isrnmeas  34886  dya2iocucvr  34969  sxbrsigalem1  34970  eulerpartlemt  35056  bnj1398  35717  bnj1498  35744  fnrelpredd  35781  dfac16  35825  acwer1prc  35831  jf1o  35965  wevgblacfn  35993  satfrnmapom  36256  gonar  36281  goalr  36283  satffun  36295  mthmblem  36466  mblfinlem3  38717  ismblfin  38719  volsupnfl  38723  itg2addnclem  38729  itg2addnc  38732  dfprop1  38785  cover2  38789  prtlem16  40066  rexzrexnn0  43951  isnumbasgrplem2  44246  dgraalem  44287  onsucrn  44413  dflim5  44471  dfno2  44569  rp-isfinite5  44658  mnurndlem1  45405  grumnudlem  45409  gruex  45422  islptre  46770  stirlinglem13  47235  stirlinglem14  47236  stirling  47238  etransc  47432  ovolval4lem2  47799  sprsymrelf1lem  48712  sprsymrelfolem2  48714  prmdvdsfmtnof  48810  prmdvdsfmtnof1  48811  perfectALTV  48960  tgoldbach  49054  uspgrsprf  49383  2zlidl  49476  2zrngamgm  49481  ply1mulgsumlem1  49637  ply1mulgsumlem2  49638  lincsumcl  49682  lincscmcl  49683  ellcoellss  49686  sepfsepc  50181  seppcld  50183