Theorem rexlimiva 3240

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 416	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))
3	2	rexlimiv 3239	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2111  ∃wrex 3107

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 1911

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-ral 3111  df-rex 3112

This theorem is referenced by:  rexraleqim  3588  rexopabb  5380  unon  7526  tfrlem16  8012  oawordeulem  8163  nneob  8262  ominf  8714  unfilem1  8766  pwfi  8803  fival  8860  elfi2  8862  fi0  8868  fiin  8870  djuss  9333  djuun  9339  updjud  9347  finnum  9361  dif1card  9421  fseqenlem2  9436  dfac8alem  9440  alephfp  9519  cflim2  9674  isfin1-3  9797  fin67  9806  isfin7-2  9807  axdc3lem  9861  axdc3lem2  9862  iunfo  9950  iundom2g  9951  winainflem  10104  rankcf  10188  map2psrpr  10521  supsrlem  10522  1re  10630  0re  10632  00id  10804  addid1  10809  0cnALT  10863  om2uzrani  13315  uzrdgfni  13321  wrdf  13862  rexanuz  14697  r19.2uz  14703  fsum2dlem  15117  fsumcom2  15121  fprod2dlem  15326  fprodcom2  15330  0dvds  15622  even2n  15683  m1expe  15715  m1exp1  15717  modprm0  16132  cshwsidrepsw  16419  smndex1basss  18062  smndex1mgm  18064  smndex1mndlem  18066  dfgrp2  18120  psgndiflemA  20290  ppttop  21612  epttop  21614  neips  21718  lmmo  21985  2ndctop  22052  2ndcsep  22064  fbncp  22444  fgcl  22483  filuni  22490  tgioo  23401  zcld  23418  cphsscph  23855  elovolm  24079  nulmbl2  24140  ellimc3  24482  limcflf  24484  pilem3  25048  perfect  25815  2vmadivsum  26125  selberg3lem2  26142  selberg4  26145  pntrsumbnd2  26151  pntrlog2bndlem3  26163  pntrlog2bndlem4  26164  pntpbnd  26172  pnt3  26196  axcontlem12  26769  axcont  26770  clwwlkn1loopb  27828  eleclclwwlkn  27861  uhgr3cyclex  27967  frgrreggt1  28178  norm1exi  29033  nmcexi  29809  lnconi  29816  pjssdif1i  29958  stri  30040  hstri  30048  stcltrthi  30061  shatomici  30141  qsxpid  30978  dispcmp  31212  isrnmeas  31569  dya2iocucvr  31652  sxbrsigalem1  31653  eulerpartlemt  31739  bnj1398  32416  bnj1498  32443  fnrelpredd  32472  satfrnmapom  32730  gonar  32755  goalr  32757  satffun  32769  mthmblem  32940  trpredlem1  33179  elno  33266  noreson  33280  nosupbnd1lem5  33325  lindsdom  35051  mblfinlem3  35096  ismblfin  35098  volsupnfl  35102  itg2addnclem  35108  itg2addnc  35111  cover2  35152  prtlem16  36165  rexzrexnn0  39745  isnumbasgrplem2  40048  dgraalem  40089  rp-isfinite5  40225  mnurndlem1  40989  grumnudlem  40993  gruex  41006  islptre  42261  stirlinglem13  42728  stirlinglem14  42729  stirling  42731  etransc  42925  ovolval4lem2  43289  sprsymrelf1lem  44008  sprsymrelfolem2  44010  prmdvdsfmtnof  44103  prmdvdsfmtnof1  44104  perfectALTV  44241  tgoldbach  44335  uspgrsprf  44374  2zlidl  44558  2zrngamgm  44563  ply1mulgsumlem1  44794  ply1mulgsumlem2  44795  lincsumcl  44840  lincscmcl  44841  ellcoellss  44844