Theorem rexlimiva 3130

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1781   ∈ wcel 2114  ∃wrex 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-ex 1782  df-rex 3062

This theorem is referenced by:  rexlimiv  3131  rexlimivw  3134  rexraleqim  3589  rexopabb  5483  unon  7782  tfrlem16  8332  oawordeulem  8489  nneob  8592  unfi  9105  ominf  9174  unfilem1  9215  fival  9325  elfi2  9327  fi0  9333  fiin  9335  djuss  9844  djuun  9850  updjud  9858  finnum  9872  dif1card  9932  fseqenlem2  9947  dfac8alem  9951  alephfp  10030  cflim2  10185  isfin1-3  10308  fin67  10317  isfin7-2  10318  axdc3lem  10372  axdc3lem2  10373  iunfo  10461  iundom2g  10462  winainflem  10616  rankcf  10700  map2psrpr  11033  supsrlem  11034  1re  11144  0re  11146  00id  11321  addrid  11326  0cnALT  11381  om2uzrani  13914  uzrdgfni  13920  wrdf  14480  rexanuz  15308  r19.2uz  15314  fsum2dlem  15732  fsumcom2  15736  fprod2dlem  15945  fprodcom2  15949  0dvds  16245  even2n  16311  m1expe  16343  m1exp1  16345  modprm0  16776  cshwsidrepsw  17064  smndex1basss  18876  smndex1mgm  18878  smndex1mndlem  18880  dfgrp2  18938  pzriprnglem4  21464  psgndiflemA  21581  ppttop  22972  epttop  22974  neips  23078  lmmo  23345  2ndctop  23412  2ndcsep  23424  fbncp  23804  fgcl  23843  filuni  23850  tgioo  24761  zcld  24779  cphsscph  25218  elovolm  25442  nulmbl2  25503  ellimc3  25846  limcflf  25848  pilem3  26418  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  29044  axcont  29045  clwwlkn1loopb  30113  eleclclwwlkn  30146  uhgr3cyclex  30252  frgrreggt1  30463  norm1exi  31321  nmcexi  32097  lnconi  32104  pjssdif1i  32246  stri  32328  hstri  32336  stcltrthi  32349  shatomici  32429  qsxpid  33422  dispcmp  34003  isrnmeas  34344  dya2iocucvr  34428  sxbrsigalem1  34429  eulerpartlemt  34515  bnj1398  35176  bnj1498  35203  fnrelpredd  35234  r1omfi  35248  wevgblacfn  35291  satfrnmapom  35552  gonar  35577  goalr  35579  satffun  35591  mthmblem  35762  lindsdom  37935  mblfinlem3  37980  ismblfin  37982  volsupnfl  37986  itg2addnclem  37992  itg2addnc  37995  cover2  38036  prtlem16  39315  rexzrexnn0  43232  isnumbasgrplem2  43532  dgraalem  43573  onsucrn  43699  dflim5  43757  dfno2  43855  rp-isfinite5  43944  mnurndlem1  44708  grumnudlem  44712  gruex  44725  islptre  46049  stirlinglem13  46514  stirlinglem14  46515  stirling  46517  etransc  46711  ovolval4lem2  47078  sprsymrelf1lem  47951  sprsymrelfolem2  47953  prmdvdsfmtnof  48049  prmdvdsfmtnof1  48050  perfectALTV  48199  tgoldbach  48293  uspgrsprf  48622  2zlidl  48716  2zrngamgm  48721  ply1mulgsumlem1  48862  ply1mulgsumlem2  48863  lincsumcl  48907  lincscmcl  48908  ellcoellss  48911  sepfsepc  49403  seppcld  49405