Theorem rexlimiva 2785

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 424	. 2 |- ( x e. A -> ( ph -> ps ) )
3	2	rexlimiv 2784	1 |- ( E. x e. A ph -> ps )

Syntax hints:   -> wi 4   /\ wa 359   e. wcel 1721   E.wrex 2667

This theorem is referenced by:  unon  4770  tfrlem16  6613  oawordeulem  6756  nneob  6854  ominf  7280  unfilem1  7330  pwfi  7360  fival  7375  elfi2  7377  fi0  7383  fiin  7385  finnum  7791  dif1card  7848  fseqenlem2  7862  dfac8alem  7866  alephfp  7945  cflim2  8099  isfin1-3  8222  fin67  8231  isfin7-2  8232  axdc3lem  8286  axdc3lem2  8287  iunfo  8370  iundom2g  8371  winainflem  8524  rankcf  8608  map2psrpr  8941  supsrlem  8942  1re  9046  00id  9197  addid1  9202  om2uzrani  11247  uzrdgfni  11253  wrdf  11688  rexanuz  12104  r19.2uz  12110  fsum2dlem  12509  fsumcom2  12513  0dvds  12825  ppttop  17026  epttop  17028  neips  17132  lmmo  17398  2ndctop  17463  2ndcsep  17475  fbncp  17824  fgcl  17863  filuni  17870  tgioo  18780  zcld  18797  elovolm  19324  nulmbl2  19384  ellimc3  19719  limcflf  19721  pilem3  20322  perfect  20968  2vmadivsum  21188  selberg3lem2  21205  selberg4  21208  pntrsumbnd2  21214  pntrlog2bndlem3  21226  pntrlog2bndlem4  21227  pntpbnd  21235  pnt3  21259  norm1exi  22705  nmcexi  23482  lnconi  23489  pjssdif1i  23631  stri  23713  hstri  23721  stcltrthi  23734  shatomici  23814  isrnmeas  24507  dya2iocucvr  24587  sxbrsigalem1  24588  fprod2dlem  25257  fprodcom2  25261  trpredlem1  25444  elno  25514  noreson  25528  axcontlem12  25818  axcont  25819  mblfinlem2  26144  ismblfin  26146  volsupnfl  26150  itg2addnclem  26155  itg2addnc  26158  cover2  26305  prtlem16  26608  rexzrexnn0  26754  isnumbasgrplem2  27137  dgraalem  27218  stirlinglem13  27702  stirlinglem14  27703  stirling  27705  bnj1398  29109  bnj1498  29136

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-11 1757

This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-ral 2671  df-rex 2672