Theorem rexlimiva 3136

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

Syntax hints:   → wi 4   ∧ wa 394  ∃wex 1773   ∈ wcel 2098  ∃wrex 3059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905

This theorem depends on definitions:  df-bi 206  df-ex 1774  df-rex 3060

This theorem is referenced by:  rexlimiv  3137  rexlimivw  3140  rexraleqim  3630  rexopabb  5530  unon  7835  tfrlem16  8414  oawordeulem  8575  nneob  8677  unfi  9197  ominf  9283  ominfOLD  9284  unfilem1  9335  pwfiOLD  9373  fival  9437  elfi2  9439  fi0  9445  fiin  9447  djuss  9945  djuun  9951  updjud  9959  finnum  9973  dif1card  10035  fseqenlem2  10050  dfac8alem  10054  alephfp  10133  cflim2  10288  isfin1-3  10411  fin67  10420  isfin7-2  10421  axdc3lem  10475  axdc3lem2  10476  iunfo  10564  iundom2g  10565  winainflem  10718  rankcf  10802  map2psrpr  11135  supsrlem  11136  1re  11246  0re  11248  00id  11421  addrid  11426  0cnALT  11480  om2uzrani  13953  uzrdgfni  13959  wrdf  14505  rexanuz  15328  r19.2uz  15334  fsum2dlem  15752  fsumcom2  15756  fprod2dlem  15960  fprodcom2  15964  0dvds  16257  even2n  16322  m1expe  16354  m1exp1  16356  modprm0  16777  cshwsidrepsw  17066  smndex1basss  18865  smndex1mgm  18867  smndex1mndlem  18869  dfgrp2  18927  pzriprnglem4  21427  psgndiflemA  21550  ppttop  22954  epttop  22956  neips  23061  lmmo  23328  2ndctop  23395  2ndcsep  23407  fbncp  23787  fgcl  23826  filuni  23833  tgioo  24756  zcld  24773  cphsscph  25223  elovolm  25448  nulmbl2  25509  ellimc3  25852  limcflf  25854  pilem3  26435  perfect  27209  2vmadivsum  27519  selberg3lem2  27536  selberg4  27539  pntrsumbnd2  27545  pntrlog2bndlem3  27557  pntrlog2bndlem4  27558  pntpbnd  27566  pnt3  27590  elnoOLD  27625  noreson  27639  nosupbnd1lem5  27691  noinfbnd1lem5  27706  axcontlem12  28858  axcont  28859  clwwlkn1loopb  29925  eleclclwwlkn  29958  uhgr3cyclex  30064  frgrreggt1  30275  norm1exi  31132  nmcexi  31908  lnconi  31915  pjssdif1i  32057  stri  32139  hstri  32147  stcltrthi  32160  shatomici  32240  qsxpid  33173  dispcmp  33591  isrnmeas  33950  dya2iocucvr  34035  sxbrsigalem1  34036  eulerpartlemt  34122  bnj1398  34796  bnj1498  34823  fnrelpredd  34843  satfrnmapom  35111  gonar  35136  goalr  35138  satffun  35150  mthmblem  35321  lindsdom  37218  mblfinlem3  37263  ismblfin  37265  volsupnfl  37269  itg2addnclem  37275  itg2addnc  37278  cover2  37319  prtlem16  38471  rexzrexnn0  42366  isnumbasgrplem2  42670  dgraalem  42711  onsucrn  42842  dflim5  42900  dfno2  43000  rp-isfinite5  43089  mnurndlem1  43860  grumnudlem  43864  gruex  43877  islptre  45145  stirlinglem13  45612  stirlinglem14  45613  stirling  45615  etransc  45809  ovolval4lem2  46176  sprsymrelf1lem  46968  sprsymrelfolem2  46970  prmdvdsfmtnof  47063  prmdvdsfmtnof1  47064  perfectALTV  47200  tgoldbach  47294  uspgrsprf  47394  2zlidl  47488  2zrngamgm  47493  ply1mulgsumlem1  47640  ply1mulgsumlem2  47641  lincsumcl  47685  lincscmcl  47686  ellcoellss  47689  sepfsepc  48132  seppcld  48134