Theorem rexlimiva 3159

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∃wex 1812   ∈ wcel 2147  ∃wrex 3090

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 1945

This proof depends on definitions:  df-bi 210  df-ex 1813  df-rex 3091

This theorem is used by:  rexlimiv  3160  rexlimivw  3163  rexraleqim  3604  rexopabb  5509  unon  7876  tfrlem16  8439  oawordeulem  8600  nneob  8703  unfi  9224  ominf  9293  unfilem1  9335  fival  9441  elfi2  9443  fi0  9449  fiin  9451  hffi  9946  djuss  10038  djuun  10044  updjud  10052  finnum  10066  dif1card  10128  fseqenlem2  10143  dfac8alem  10147  alephfp  10226  cflim2  10380  isfin1-3  10503  fin67  10512  isfin7-2  10513  axdc3lem  10567  axdc3lem2  10568  iunfo  10662  iundom2g  10663  winainflem  10817  rankcf  10901  map2psrpr  11234  supsrlem  11235  1re  11347  0re  11349  00id  11524  addrid  11529  0cnALT  11584  om2uzrani  14135  uzrdgfni  14141  wrdf  14704  rexanuz  15557  r19.2uz  15563  fsum2dlem  15980  fsumcom2  15984  fprod2dlem  16191  fprodcom2  16195  0dvds  16490  even2n  16556  m1expe  16588  m1exp1  16590  modprm0  17027  cshwsidrepsw  17315  smndex1basss  19154  smndex1mgm  19156  smndex1mndlem  19158  dfgrp2  19223  qsxpid  19437  pzriprnglem4  21845  psgndiflemA  21962  lindsdom  22211  ppttop  23380  epttop  23382  neips  23486  lmmo  23753  2ndctop  23820  2ndcsep  23833  fbncp  24213  fgcl  24252  filuni  24259  tgioo  25170  zcld  25188  cphsscph  25627  elovolm  25851  nulmbl2  25912  ellimc3  26254  limcflf  26256  rnplynfin  26685  plyconz  26686  pilem3  26837  perfect  27615  2vmadivsum  27925  selberg3lem2  27942  selberg4  27945  pntrsumbnd2  27951  pntrlog2bndlem3  27963  pntrlog2bndlem4  27964  pntpbnd  27972  pnt3  27996  noreson  28074  nosupbnd1lem5  28126  noinfbnd1lem5  28141  axcontlem12  29610  axcont  29611  clwwlkn1loopb  30691  eleclclwwlkn  30724  uhgr3cyclex  30840  frgrreggt1  31051  norm1exi  31909  nmcexi  32685  lnconi  32692  pjssdif1i  32834  stri  32916  hstri  32924  stcltrthi  32937  shatomici  33017  dispcmp  34602  isrnmeas  34944  dya2iocucvr  35027  sxbrsigalem1  35028  eulerpartlemt  35114  bnj1398  35775  bnj1498  35802  fnrelpredd  35845  dfac16  35887  acwer1prc  35893  jf1o  36052  wevgblacfn  36080  satfrnmapom  36343  gonar  36368  goalr  36370  satffun  36382  mthmblem  36553  mblfinlem3  38845  ismblfin  38847  volsupnfl  38851  itg2addnclem  38857  itg2addnc  38860  dfprop1  38913  cover2  38917  prtlem16  40192  rexzrexnn0  44077  isnumbasgrplem2  44371  dgraalem  44412  onsucrn  44534  dflim5  44592  dfno2  44690  rp-isfinite5  44779  mnurndlem1  45526  grumnudlem  45530  gruex  45543  islptre  46904  stirlinglem13  47369  stirlinglem14  47370  stirling  47372  etransc  47566  ovolval4lem2  47933  sprsymrelf1lem  48846  sprsymrelfolem2  48848  prmdvdsfmtnof  48944  prmdvdsfmtnof1  48945  perfectALTV  49094  tgoldbach  49188  uspgrsprf  49517  2zlidl  49610  2zrngamgm  49615  ply1mulgsumlem1  49829  ply1mulgsumlem2  49830  lincsumcl  49874  lincscmcl  49875  ellcoellss  49878  sepfsepc  50373  seppcld  50375