Theorem rexlimiva 2887

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

Hypothesis

Ref	Expression
rexlimiva.1	|- ( ( x e. A /\ ph ) -> ps )

Assertion

Ref	Expression
rexlimiva	|- ( E. x e. A ph -> ps )

Distinct variable group:   ps, x

Allowed substitution hints:   ph( x)   A( x)

Proof of Theorem rexlimiva

Step	Hyp	Ref	Expression
1		rexlimiva.1	. . 3 |- ( ( x e. A /\ ph ) -> ps )
2	1	ex 440	. 2 |- ( x e. A -> ( ph -> ps ) )
3	2	rexlimiv 2885	1 |- ( E. x e. A ph -> ps )

Syntax hints:   -> wi 4   /\ wa 375   e. wcel 1898   E.wrex 2750

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769

This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1675  df-ral 2754  df-rex 2755

This theorem is referenced by:  rexraleqim  3177  unon  6685  tfrlem16  7137  oawordeulem  7281  nneob  7379  ominf  7810  unfilem1  7861  pwfi  7895  fival  7952  elfi2  7954  fi0  7960  fiin  7962  finnum  8408  dif1card  8467  fseqenlem2  8482  dfac8alem  8486  alephfp  8565  cflim2  8719  isfin1-3  8842  fin67  8851  isfin7-2  8852  axdc3lem  8906  axdc3lem2  8907  iunfo  8990  iundom2g  8991  winainflem  9144  rankcf  9228  map2psrpr  9560  supsrlem  9561  1re  9668  00id  9834  addid1  9839  om2uzrani  12198  uzrdgfni  12204  wrdf  12709  rexanuz  13457  r19.2uz  13463  fsum2dlem  13880  fsumcom2  13884  fprod2dlem  14083  fprodcom2  14087  0dvds  14372  modprm0  14805  cshwsidrepsw  15113  psgndiflemA  19218  ppttop  20071  epttop  20073  neips  20178  lmmo  20445  2ndctop  20511  2ndcsep  20523  fbncp  20903  fgcl  20942  filuni  20949  tgioo  21863  zcld  21880  elovolm  22477  nulmbl2  22539  ellimc3  22883  limcflf  22885  pilem3  23458  pilem3OLD  23459  perfect  24208  2vmadivsum  24428  selberg3lem2  24445  selberg4  24448  pntrsumbnd2  24454  pntrlog2bndlem3  24466  pntrlog2bndlem4  24467  pntpbnd  24475  pnt3  24499  axcontlem12  25054  axcont  25055  eleclclwwlkn  25610  frgrareggt1  25893  norm1exi  26952  nmcexi  27728  lnconi  27735  pjssdif1i  27877  stri  27959  hstri  27967  stcltrthi  27980  shatomici  28060  dispcmp  28735  isrnmeas  29071  dya2iocucvr  29155  sxbrsigalem1  29156  eulerpartlemt  29253  bnj1398  29892  bnj1498  29919  mthmblem  30267  trpredlem1  30517  elno  30582  noreson  30596  mblfinlem3  32024  ismblfin  32026  volsupnfl  32030  dvtanlemOLD  32036  itg2addnclem  32038  itg2addnc  32041  cover2  32085  prtlem16  32486  rexzrexnn0  35692  isnumbasgrplem2  36008  dgraalem  36052  dgraalemOLD  36053  rp-isfinite5  36207  islptre  37737  stirlinglem13  37986  stirlinglem14  37987  stirling  37989  etransc  38187  perfectALTV  38883  tgblthelfgott  38946  tgoldbach  38949  issn  39035  uhgr3cyclex  39923  2zlidl  40207  2zrngamgm  40212  ply1mulgsumlem1  40451  ply1mulgsumlem2  40452  lincsumcl  40497  lincscmcl  40498  ellcoellss  40501