Theorem rexlimiva 3155

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

Syntax hints:   → wi 4   ∧ wa 399  ∃wex 1799   ∈ wcel 2142  ∃wrex 3086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930

This theorem depends on definitions:  df-bi 209  df-ex 1800  df-rex 3087

This theorem is referenced by:  rexlimiv  3156  rexlimivw  3159  rexraleqim  3606  rexopabb  5498  unon  7811  tfrlem16  8364  oawordeulem  8523  nneob  8626  unfi  9139  ominf  9208  unfilem1  9249  fival  9358  elfi2  9360  fi0  9366  fiin  9368  djuss  9878  djuun  9884  updjud  9892  finnum  9906  dif1card  9966  fseqenlem2  9981  dfac8alem  9985  alephfp  10064  cflim2  10220  isfin1-3  10343  fin67  10352  isfin7-2  10353  axdc3lem  10407  axdc3lem2  10408  iunfo  10496  iundom2g  10497  winainflem  10651  rankcf  10735  map2psrpr  11068  supsrlem  11069  1re  11181  0re  11183  00id  11358  addrid  11363  0cnALT  11418  om2uzrani  13965  uzrdgfni  13971  wrdf  14531  rexanuz  15373  r19.2uz  15379  fsum2dlem  15797  fsumcom2  15801  fprod2dlem  16010  fprodcom2  16014  0dvds  16310  even2n  16376  m1expe  16408  m1exp1  16410  modprm0  16841  cshwsidrepsw  17129  smndex1basss  18942  smndex1mgm  18944  smndex1mndlem  18946  dfgrp2  19004  pzriprnglem4  21536  psgndiflemA  21653  ppttop  23067  epttop  23069  neips  23173  lmmo  23440  2ndctop  23507  2ndcsep  23519  fbncp  23899  fgcl  23938  filuni  23945  tgioo  24856  zcld  24874  cphsscph  25313  elovolm  25537  nulmbl2  25598  ellimc3  25941  limcflf  25943  pilem3  26516  perfect  27295  2vmadivsum  27605  selberg3lem2  27622  selberg4  27625  pntrsumbnd2  27631  pntrlog2bndlem3  27643  pntrlog2bndlem4  27644  pntpbnd  27652  pnt3  27676  noreson  27724  nosupbnd1lem5  27776  noinfbnd1lem5  27791  axcontlem12  29176  axcont  29177  clwwlkn1loopb  30245  eleclclwwlkn  30278  uhgr3cyclex  30384  frgrreggt1  30595  norm1exi  31453  nmcexi  32229  lnconi  32236  pjssdif1i  32378  stri  32460  hstri  32468  stcltrthi  32481  shatomici  32561  qsxpid  33548  dispcmp  34156  isrnmeas  34497  dya2iocucvr  34581  sxbrsigalem1  34582  eulerpartlemt  34668  bnj1398  35329  bnj1498  35356  fnrelpredd  35387  r1omfi  35401  wevgblacfn  35454  satfrnmapom  35720  gonar  35745  goalr  35747  satffun  35759  mthmblem  35930  lindsdom  38113  mblfinlem3  38158  ismblfin  38160  volsupnfl  38164  itg2addnclem  38170  itg2addnc  38173  cover2  38214  prtlem16  39493  rexzrexnn0  43381  isnumbasgrplem2  43681  dgraalem  43722  onsucrn  43848  dflim5  43906  dfno2  44004  rp-isfinite5  44093  mnurndlem1  44857  grumnudlem  44861  gruex  44874  islptre  46195  stirlinglem13  46660  stirlinglem14  46661  stirling  46663  etransc  46857  ovolval4lem2  47224  sprsymrelf1lem  48097  sprsymrelfolem2  48099  prmdvdsfmtnof  48195  prmdvdsfmtnof1  48196  perfectALTV  48345  tgoldbach  48439  uspgrsprf  48768  2zlidl  48862  2zrngamgm  48867  ply1mulgsumlem1  49008  ply1mulgsumlem2  49009  lincsumcl  49053  lincscmcl  49054  ellcoellss  49057  sepfsepc  49549  seppcld  49551