Theorem rexlimiva 2826

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-12 1791

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-ral 2710  df-rex 2711

This theorem is referenced by:  rexraleqim  3074  unon  6431  tfrlem16  6838  oawordeulem  6981  nneob  7079  ominf  7513  unfilem1  7564  pwfi  7594  fival  7650  elfi2  7652  fi0  7658  fiin  7660  finnum  8106  dif1card  8165  fseqenlem2  8183  dfac8alem  8187  alephfp  8266  cflim2  8420  isfin1-3  8543  fin67  8552  isfin7-2  8553  axdc3lem  8607  axdc3lem2  8608  iunfo  8691  iundom2g  8692  winainflem  8848  rankcf  8932  map2psrpr  9265  supsrlem  9266  1re  9373  00id  9532  addid1  9537  om2uzrani  11759  uzrdgfni  11765  wrdf  12224  rexanuz  12817  r19.2uz  12823  fsum2dlem  13221  fsumcom2  13225  0dvds  13536  modprm0  13856  cshwsidrepsw  14103  psgndiflemA  17873  ppttop  18453  epttop  18455  neips  18559  lmmo  18826  2ndctop  18893  2ndcsep  18905  fbncp  19254  fgcl  19293  filuni  19300  tgioo  20215  zcld  20232  elovolm  20800  nulmbl2  20860  ellimc3  21196  limcflf  21198  pilem3  21803  perfect  22455  2vmadivsum  22675  selberg3lem2  22692  selberg4  22695  pntrsumbnd2  22701  pntrlog2bndlem3  22713  pntrlog2bndlem4  22714  pntpbnd  22722  pnt3  22746  axcontlem12  23044  axcont  23045  norm1exi  24476  nmcexi  25253  lnconi  25260  pjssdif1i  25402  stri  25484  hstri  25492  stcltrthi  25505  shatomici  25585  isrnmeas  26468  dya2iocucvr  26553  sxbrsigalem1  26554  eulerpartlemt  26602  fprod2dlem  27338  fprodcom2  27342  trpredlem1  27538  elno  27634  noreson  27648  mblfinlem3  28274  ismblfin  28276  volsupnfl  28280  dvtanlem  28285  itg2addnclem  28287  itg2addnc  28290  cover2  28451  prtlem16  28859  rexzrexnn0  28987  isnumbasgrplem2  29305  dgraalem  29347  stirlinglem13  29727  stirlinglem14  29728  stirling  29730  eleclclwwlkn  30353  frgrareggt1  30555  lincsumcl  30674  lincscmcl  30675  ellcoellss  30678  bnj1398  31727  bnj1498  31754