Theorem rexlimiva 3028

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

Syntax hints:   -> wi 4   /\ wa 384   e. wcel 1990   E.wrex 2913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-ral 2917  df-rex 2918

This theorem is referenced by:  rexraleqim  3328  unon  7031  tfrlem16  7489  oawordeulem  7634  nneob  7732  ominf  8172  unfilem1  8224  pwfi  8261  fival  8318  elfi2  8320  fi0  8326  fiin  8328  finnum  8774  dif1card  8833  fseqenlem2  8848  dfac8alem  8852  alephfp  8931  cflim2  9085  isfin1-3  9208  fin67  9217  isfin7-2  9218  axdc3lem  9272  axdc3lem2  9273  iunfo  9361  iundom2g  9362  winainflem  9515  rankcf  9599  map2psrpr  9931  supsrlem  9932  1re  10039  00id  10211  addid1  10216  om2uzrani  12751  uzrdgfni  12757  wrdf  13310  rexanuz  14085  r19.2uz  14091  fsum2dlem  14501  fsumcom2  14505  fsumcom2OLD  14506  fprod2dlem  14710  fprodcom2  14714  fprodcom2OLD  14715  0dvds  15002  even2n  15066  m1expe  15091  m1exp1  15093  modprm0  15510  cshwsidrepsw  15800  dfgrp2  17447  psgndiflemA  19947  ppttop  20811  epttop  20813  neips  20917  lmmo  21184  2ndctop  21250  2ndcsep  21262  fbncp  21643  fgcl  21682  filuni  21689  tgioo  22599  zcld  22616  elovolm  23243  nulmbl2  23304  ellimc3  23643  limcflf  23645  pilem3  24207  perfect  24956  2vmadivsum  25230  selberg3lem2  25247  selberg4  25250  pntrsumbnd2  25256  pntrlog2bndlem3  25268  pntrlog2bndlem4  25269  pntpbnd  25277  pnt3  25301  axcontlem12  25855  axcont  25856  eleclclwwlksn  26953  uhgr3cyclex  27042  frgrreggt1  27251  norm1exi  28107  nmcexi  28885  lnconi  28892  pjssdif1i  29034  stri  29116  hstri  29124  stcltrthi  29137  shatomici  29217  dispcmp  29926  isrnmeas  30263  dya2iocucvr  30346  sxbrsigalem1  30347  eulerpartlemt  30433  bnj1398  31102  bnj1498  31129  mthmblem  31477  trpredlem1  31727  elno  31799  noreson  31813  nosupbnd1lem5  31858  lindsdom  33403  mblfinlem3  33448  ismblfin  33450  volsupnfl  33454  itg2addnclem  33461  itg2addnc  33464  cover2  33508  prtlem16  34154  rexzrexnn0  37368  isnumbasgrplem2  37674  dgraalem  37715  rp-isfinite5  37863  islptre  39851  stirlinglem13  40303  stirlinglem14  40304  stirling  40306  etransc  40500  ovolval4lem2  40864  prmdvdsfmtnof  41498  prmdvdsfmtnof1  41499  perfectALTV  41632  tgoldbach  41705  tgblthelfgottOLD  41709  tgoldbachOLD  41712  sprsymrelf1lem  41741  sprsymrelfolem2  41743  uspgrsprf  41754  2zlidl  41934  2zrngamgm  41939  ply1mulgsumlem1  42174  ply1mulgsumlem2  42175  lincsumcl  42220  lincscmcl  42221  ellcoellss  42224