Theorem rexlimiva 2942

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

Syntax hints:   -> wi 4   /\ wa 367   e. wcel 1823   E.wrex 2805

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709

This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1618  df-ral 2809  df-rex 2810

This theorem is referenced by:  rexraleqim  3222  unon  6639  tfrlem16  7054  oawordeulem  7195  nneob  7293  ominf  7725  unfilem1  7776  pwfi  7807  fival  7864  elfi2  7866  fi0  7872  fiin  7874  finnum  8320  dif1card  8379  fseqenlem2  8397  dfac8alem  8401  alephfp  8480  cflim2  8634  isfin1-3  8757  fin67  8766  isfin7-2  8767  axdc3lem  8821  axdc3lem2  8822  iunfo  8905  iundom2g  8906  winainflem  9060  rankcf  9144  map2psrpr  9476  supsrlem  9477  1re  9584  00id  9744  addid1  9749  om2uzrani  12045  uzrdgfni  12051  wrdf  12538  rexanuz  13260  r19.2uz  13266  fsum2dlem  13667  fsumcom2  13671  fprod2dlem  13866  fprodcom2  13870  0dvds  14088  modprm0  14414  cshwsidrepsw  14662  psgndiflemA  18810  ppttop  19675  epttop  19677  neips  19781  lmmo  20048  2ndctop  20114  2ndcsep  20126  fbncp  20506  fgcl  20545  filuni  20552  tgioo  21467  zcld  21484  elovolm  22052  nulmbl2  22113  ellimc3  22449  limcflf  22451  pilem3  23014  perfect  23704  2vmadivsum  23924  selberg3lem2  23941  selberg4  23944  pntrsumbnd2  23950  pntrlog2bndlem3  23962  pntrlog2bndlem4  23963  pntpbnd  23971  pnt3  23995  axcontlem12  24480  axcont  24481  eleclclwwlkn  25035  frgrareggt1  25318  norm1exi  26366  nmcexi  27143  lnconi  27150  pjssdif1i  27292  stri  27374  hstri  27382  stcltrthi  27395  shatomici  27475  dispcmp  28097  isrnmeas  28408  dya2iocucvr  28492  sxbrsigalem1  28493  eulerpartlemt  28574  mthmblem  29204  trpredlem1  29550  elno  29646  noreson  29660  mblfinlem3  30293  ismblfin  30295  volsupnfl  30299  dvtanlem  30304  itg2addnclem  30306  itg2addnc  30309  cover2  30444  prtlem16  30850  rexzrexnn0  30977  isnumbasgrplem2  31294  dgraalem  31335  islptre  31864  stirlinglem13  32107  stirlinglem14  32108  stirling  32110  etransc  32305  2zlidl  32994  2zrngamgm  32999  ply1mulgsumlem1  33240  ply1mulgsumlem2  33241  lincsumcl  33286  lincscmcl  33287  ellcoellss  33290  bnj1398  34491  bnj1498  34518  rp-isfinite5  38156