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 2166  ∃wrex 3118

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1881  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  27388  eleclclwwlkn  27429  uhgr3cyclex  27558  frgrreggt1  27808  norm1exi  28662  nmcexi  29440  lnconi  29447  pjssdif1i  29589  stri  29671  hstri  29679  stcltrthi  29692  shatomici  29772  dispcmp  30471  isrnmeas  30808  dya2iocucvr  30891  sxbrsigalem1  30892  eulerpartlemt  30978  bnj1398  31648  bnj1498  31675  mthmblem  32023  trpredlem1  32265  elno  32338  noreson  32352  nosupbnd1lem5  32397  lindsdom  33947  mblfinlem3  33992  ismblfin  33994  volsupnfl  33998  itg2addnclem  34004  itg2addnc  34007  cover2  34051  prtlem16  34944  rexzrexnn0  38212  isnumbasgrplem2  38517  dgraalem  38558  rp-isfinite5  38704  islptre  40646  stirlinglem13  41097  stirlinglem14  41098  stirling  41100  etransc  41294  ovolval4lem2  41658  prmdvdsfmtnof  42328  prmdvdsfmtnof1  42329  perfectALTV  42462  tgoldbach  42535  sprsymrelf1lem  42588  sprsymrelfolem2  42590  uspgrsprf  42601  2zlidl  42781  2zrngamgm  42786  ply1mulgsumlem1  43021  ply1mulgsumlem2  43022  lincsumcl  43067  lincscmcl  43068  ellcoellss  43071