Theorem rexlimiva 2589

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

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2148   E.wrex 2456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-i5r 1535

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460  df-rex 2461

This theorem is referenced by:  unon  4512  reg2exmidlema  4535  ssfilem  6878  diffitest  6890  fival  6972  elfi2  6974  fi0  6977  djuss  7072  updjud  7084  enumct  7117  finnum  7185  dmaddpqlem  7379  nqpi  7380  nq0nn  7444  recexprlemm  7626  rexanuz  11000  r19.2uz  11005  maxleast  11225  fsum2dlemstep  11445  fisumcom2  11449  fprod2dlemstep  11633  fprodcom2fi  11637  0dvds  11821  even2n  11882  m1expe  11907  m1exp1  11909  modprm0  12257  dfgrp2  12910  epttop  13778  neipsm  13842  tgioo  14234  sin0pilem2  14391  pilem3  14392  bj-nn0suc  14904  bj-nn0sucALT  14918  trirec0xor  14982