Theorem rexlimiva 2599

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 2598	1 |- ( E. x e. A ph -> ps )

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

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 1457  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-4 1520  ax-17 1536  ax-ial 1544  ax-i5r 1545

This theorem depends on definitions:  df-bi 117  df-nf 1471  df-ral 2470  df-rex 2471

This theorem is referenced by:  unon  4522  reg2exmidlema  4545  ssfilem  6888  diffitest  6900  fival  6982  elfi2  6984  fi0  6987  djuss  7082  updjud  7094  enumct  7127  finnum  7195  dmaddpqlem  7389  nqpi  7390  nq0nn  7454  recexprlemm  7636  rexanuz  11010  r19.2uz  11015  maxleast  11235  fsum2dlemstep  11455  fisumcom2  11459  fprod2dlemstep  11643  fprodcom2fi  11647  0dvds  11831  even2n  11892  m1expe  11917  m1exp1  11919  modprm0  12267  dfgrp2  12923  epttop  13861  neipsm  13925  tgioo  14317  sin0pilem2  14474  pilem3  14475  bj-nn0suc  14987  bj-nn0sucALT  15001  trirec0xor  15065