Theorem rexlimiva 2484

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

Syntax hints:   -> wi 4   /\ wa 102   e. wcel 1438   E.wrex 2360

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472  ax-i5r 1473

This theorem depends on definitions:  df-bi 115  df-nf 1395  df-ral 2364  df-rex 2365

This theorem is referenced by:  unon  4328  reg2exmidlema  4350  ssfilem  6591  diffitest  6603  djuun  6760  djuss  6761  updjud  6773  finnum  6811  dmaddpqlem  6936  nqpi  6937  nq0nn  7001  recexprlemm  7183  rexanuz  10421  r19.2uz  10426  maxleast  10646  fsum2dlemstep  10828  fisumcom2  10832  0dvds  11094  even2n  11152  m1expe  11177  m1exp1  11179  bj-nn0suc  11859  bj-nn0sucALT  11873