Theorem rexlimiva 3237

Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 18-Dec-2006.)

Hypothesis

Ref	Expression
rexlimiva.1	⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓)

Assertion

Ref	Expression
rexlimiva	⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

Distinct variable group:   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝐴(𝑥)

Proof of Theorem rexlimiva

Step	Hyp	Ref	Expression
1		rexlimiva.1	. . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜓)
2	1	ex 403	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))
3	2	rexlimiv 3236	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ wa 386   ∈ wcel 2164  ∃wrex 3118

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1879  df-ral 3122  df-rex 3123

This theorem is referenced by:  rexraleqim  3546  unon  7292  tfrlem16  7755  oawordeulem  7901  nneob  7999  ominf  8441  unfilem1  8493  pwfi  8530  fival  8587  elfi2  8589  fi0  8595  fiin  8597  djuss  9059  djuun  9065  updjud  9073  finnum  9087  dif1card  9146  fseqenlem2  9161  dfac8alem  9165  alephfp  9244  cflim2  9400  isfin1-3  9523  fin67  9532  isfin7-2  9533  axdc3lem  9587  axdc3lem2  9588  iunfo  9676  iundom2g  9677  winainflem  9830  rankcf  9914  map2psrpr  10247  supsrlem  10248  1re  10356  0re  10358  00id  10530  addid1  10535  0cnALT  10589  om2uzrani  13046  uzrdgfni  13052  wrdf  13579  rexanuz  14462  r19.2uz  14468  fsum2dlem  14876  fsumcom2  14880  fprod2dlem  15083  fprodcom2  15087  0dvds  15379  even2n  15440  m1expe  15465  m1exp1  15467  modprm0  15881  cshwsidrepsw  16166  dfgrp2  17801  psgndiflemA  20307  ppttop  21182  epttop  21184  neips  21288  lmmo  21555  2ndctop  21621  2ndcsep  21633  fbncp  22013  fgcl  22052  filuni  22059  tgioo  22969  zcld  22986  cphsscph  23419  elovolm  23641  nulmbl2  23702  ellimc3  24042  limcflf  24044  pilem3  24606  pilem3OLD  24607  perfect  25369  2vmadivsum  25643  selberg3lem2  25660  selberg4  25663  pntrsumbnd2  25669  pntrlog2bndlem3  25681  pntrlog2bndlem4  25682  pntpbnd  25690  pnt3  25714  axcontlem12  26274  axcont  26275  clwwlkn1loopb  27382  eleclclwwlkn  27422  uhgr3cyclex  27547  frgrreggt1  27797  norm1exi  28651  nmcexi  29429  lnconi  29436  pjssdif1i  29578  stri  29660  hstri  29668  stcltrthi  29681  shatomici  29761  dispcmp  30460  isrnmeas  30797  dya2iocucvr  30880  sxbrsigalem1  30881  eulerpartlemt  30967  bnj1398  31637  bnj1498  31664  mthmblem  32012  trpredlem1  32254  elno  32327  noreson  32341  nosupbnd1lem5  32386  lindsdom  33940  mblfinlem3  33985  ismblfin  33987  volsupnfl  33991  itg2addnclem  33997  itg2addnc  34000  cover2  34044  prtlem16  34937  rexzrexnn0  38205  isnumbasgrplem2  38510  dgraalem  38551  rp-isfinite5  38697  islptre  40639  stirlinglem13  41090  stirlinglem14  41091  stirling  41093  etransc  41287  ovolval4lem2  41651  prmdvdsfmtnof  42321  prmdvdsfmtnof1  42322  perfectALTV  42455  tgoldbach  42528  sprsymrelf1lem  42581  sprsymrelfolem2  42583  uspgrsprf  42594  2zlidl  42774  2zrngamgm  42779  ply1mulgsumlem1  43014  ply1mulgsumlem2  43015  lincsumcl  43060  lincscmcl  43061  ellcoellss  43064