Theorem rexlimiva 2944

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 2942	1 |- ( E. x e. A ph -> ps )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-ral 2812  df-rex 2813

This theorem is referenced by:  rexraleqim  3222  unon  6637  tfrlem16  7052  oawordeulem  7193  nneob  7291  ominf  7722  unfilem1  7773  pwfi  7804  fival  7861  elfi2  7863  fi0  7869  fiin  7871  finnum  8318  dif1card  8377  fseqenlem2  8395  dfac8alem  8399  alephfp  8478  cflim2  8632  isfin1-3  8755  fin67  8764  isfin7-2  8765  axdc3lem  8819  axdc3lem2  8820  iunfo  8903  iundom2g  8904  winainflem  9060  rankcf  9144  map2psrpr  9476  supsrlem  9477  1re  9584  00id  9743  addid1  9748  om2uzrani  12019  uzrdgfni  12025  wrdf  12506  rexanuz  13127  r19.2uz  13133  fsum2dlem  13534  fsumcom2  13538  0dvds  13854  modprm0  14178  cshwsidrepsw  14425  psgndiflemA  18397  ppttop  19267  epttop  19269  neips  19373  lmmo  19640  2ndctop  19707  2ndcsep  19719  fbncp  20068  fgcl  20107  filuni  20114  tgioo  21029  zcld  21046  elovolm  21614  nulmbl2  21675  ellimc3  22011  limcflf  22013  pilem3  22575  perfect  23227  2vmadivsum  23447  selberg3lem2  23464  selberg4  23467  pntrsumbnd2  23473  pntrlog2bndlem3  23485  pntrlog2bndlem4  23486  pntpbnd  23494  pnt3  23518  axcontlem12  23947  axcont  23948  eleclclwwlkn  24495  frgrareggt1  24779  norm1exi  25830  nmcexi  26607  lnconi  26614  pjssdif1i  26756  stri  26838  hstri  26846  stcltrthi  26859  shatomici  26939  isrnmeas  27797  dya2iocucvr  27881  sxbrsigalem1  27882  eulerpartlemt  27936  fprod2dlem  28673  fprodcom2  28677  trpredlem1  28873  elno  28969  noreson  28983  mblfinlem3  29617  ismblfin  29619  volsupnfl  29623  dvtanlem  29628  itg2addnclem  29630  itg2addnc  29633  cover2  29794  prtlem16  30201  rexzrexnn0  30328  isnumbasgrplem2  30646  dgraalem  30688  stirlinglem13  31341  stirlinglem14  31342  stirling  31344  ply1mulgsumlem1  31934  ply1mulgsumlem2  31935  lincsumcl  31980  lincscmcl  31981  ellcoellss  31984  bnj1398  33044  bnj1498  33071