Theorem rexlimiva 2839

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

Syntax hints:   -> wi 4   /\ wa 369   e. wcel 1756   E.wrex 2719

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-12 1792

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-ral 2723  df-rex 2724

This theorem is referenced by:  rexraleqim  3088  unon  6445  tfrlem16  6855  oawordeulem  6996  nneob  7094  ominf  7528  unfilem1  7579  pwfi  7609  fival  7665  elfi2  7667  fi0  7673  fiin  7675  finnum  8121  dif1card  8180  fseqenlem2  8198  dfac8alem  8202  alephfp  8281  cflim2  8435  isfin1-3  8558  fin67  8567  isfin7-2  8568  axdc3lem  8622  axdc3lem2  8623  iunfo  8706  iundom2g  8707  winainflem  8863  rankcf  8947  map2psrpr  9280  supsrlem  9281  1re  9388  00id  9547  addid1  9552  om2uzrani  11778  uzrdgfni  11784  wrdf  12243  rexanuz  12836  r19.2uz  12842  fsum2dlem  13240  fsumcom2  13244  0dvds  13556  modprm0  13876  cshwsidrepsw  14123  psgndiflemA  18034  ppttop  18614  epttop  18616  neips  18720  lmmo  18987  2ndctop  19054  2ndcsep  19066  fbncp  19415  fgcl  19454  filuni  19461  tgioo  20376  zcld  20393  elovolm  20961  nulmbl2  21021  ellimc3  21357  limcflf  21359  pilem3  21921  perfect  22573  2vmadivsum  22793  selberg3lem2  22810  selberg4  22813  pntrsumbnd2  22819  pntrlog2bndlem3  22831  pntrlog2bndlem4  22832  pntpbnd  22840  pnt3  22864  axcontlem12  23224  axcont  23225  norm1exi  24656  nmcexi  25433  lnconi  25440  pjssdif1i  25582  stri  25664  hstri  25672  stcltrthi  25685  shatomici  25765  isrnmeas  26617  dya2iocucvr  26702  sxbrsigalem1  26703  eulerpartlemt  26757  fprod2dlem  27494  fprodcom2  27498  trpredlem1  27694  elno  27790  noreson  27804  mblfinlem3  28433  ismblfin  28435  volsupnfl  28439  dvtanlem  28444  itg2addnclem  28446  itg2addnc  28449  cover2  28610  prtlem16  29017  rexzrexnn0  29145  isnumbasgrplem2  29463  dgraalem  29505  stirlinglem13  29884  stirlinglem14  29885  stirling  29887  eleclclwwlkn  30510  frgrareggt1  30712  ply1mulgsumlem1  30847  ply1mulgsumlem2  30848  lincsumcl  30968  lincscmcl  30969  ellcoellss  30972  bnj1398  32028  bnj1498  32055