Theorem rexlimiva 2852

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

Syntax hints:   -> wi 4   /\ wa 370   e. wcel 1872   E.wrex 2715

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752

This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1658  df-ral 2719  df-rex 2720

This theorem is referenced by:  rexraleqim  3140  unon  6616  tfrlem16  7066  oawordeulem  7210  nneob  7308  ominf  7737  unfilem1  7788  pwfi  7822  fival  7879  elfi2  7881  fi0  7887  fiin  7889  finnum  8334  dif1card  8393  fseqenlem2  8407  dfac8alem  8411  alephfp  8490  cflim2  8644  isfin1-3  8767  fin67  8776  isfin7-2  8777  axdc3lem  8831  axdc3lem2  8832  iunfo  8915  iundom2g  8916  winainflem  9069  rankcf  9153  map2psrpr  9485  supsrlem  9486  1re  9593  00id  9759  addid1  9764  om2uzrani  12116  uzrdgfni  12122  wrdf  12624  rexanuz  13352  r19.2uz  13358  fsum2dlem  13774  fsumcom2  13778  fprod2dlem  13977  fprodcom2  13981  0dvds  14266  modprm0  14699  cshwsidrepsw  15007  psgndiflemA  19111  ppttop  19964  epttop  19966  neips  20071  lmmo  20338  2ndctop  20404  2ndcsep  20416  fbncp  20796  fgcl  20835  filuni  20842  tgioo  21756  zcld  21773  elovolm  22370  nulmbl2  22432  ellimc3  22776  limcflf  22778  pilem3  23351  pilem3OLD  23352  perfect  24101  2vmadivsum  24321  selberg3lem2  24338  selberg4  24341  pntrsumbnd2  24347  pntrlog2bndlem3  24359  pntrlog2bndlem4  24360  pntpbnd  24368  pnt3  24392  axcontlem12  24947  axcont  24948  eleclclwwlkn  25503  frgrareggt1  25786  norm1exi  26845  nmcexi  27621  lnconi  27628  pjssdif1i  27770  stri  27852  hstri  27860  stcltrthi  27873  shatomici  27953  dispcmp  28638  isrnmeas  28974  dya2iocucvr  29058  sxbrsigalem1  29059  eulerpartlemt  29156  bnj1398  29795  bnj1498  29822  mthmblem  30170  trpredlem1  30419  elno  30484  noreson  30498  mblfinlem3  31886  ismblfin  31888  volsupnfl  31892  dvtanlemOLD  31898  itg2addnclem  31900  itg2addnc  31903  cover2  31947  prtlem16  32352  rexzrexnn0  35559  isnumbasgrplem2  35876  dgraalem  35920  dgraalemOLD  35921  rp-isfinite5  36075  islptre  37582  stirlinglem13  37831  stirlinglem14  37832  stirling  37834  etransc  38032  perfectALTV  38658  tgblthelfgott  38721  tgoldbach  38724  issn  38804  2zlidl  39535  2zrngamgm  39540  ply1mulgsumlem1  39781  ply1mulgsumlem2  39782  lincsumcl  39827  lincscmcl  39828  ellcoellss  39831