Theorem rexlimiva 2569

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

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 2128   E.wrex 2436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490  ax-17 1506  ax-ial 1514  ax-i5r 1515

This theorem depends on definitions:  df-bi 116  df-nf 1441  df-ral 2440  df-rex 2441

This theorem is referenced by:  unon  4473  reg2exmidlema  4496  ssfilem  6823  diffitest  6835  fival  6917  elfi2  6919  fi0  6922  djuss  7017  updjud  7029  enumct  7062  finnum  7121  dmaddpqlem  7300  nqpi  7301  nq0nn  7365  recexprlemm  7547  rexanuz  10900  r19.2uz  10905  maxleast  11125  fsum2dlemstep  11343  fisumcom2  11347  fprod2dlemstep  11531  fprodcom2fi  11535  0dvds  11719  even2n  11778  m1expe  11803  m1exp1  11805  modprm0  12145  epttop  12586  neipsm  12650  tgioo  13042  sin0pilem2  13199  pilem3  13200  bj-nn0suc  13636  bj-nn0sucALT  13650  trirec0xor  13713