Theorem rexlimiva 2547

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

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

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 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515  ax-i5r 1516

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-ral 2422  df-rex 2423

This theorem is referenced by:  unon  4435  reg2exmidlema  4457  ssfilem  6777  diffitest  6789  fival  6866  elfi2  6868  fi0  6871  djuss  6963  updjud  6975  enumct  7008  finnum  7056  dmaddpqlem  7209  nqpi  7210  nq0nn  7274  recexprlemm  7456  rexanuz  10792  r19.2uz  10797  maxleast  11017  fsum2dlemstep  11235  fisumcom2  11239  0dvds  11549  even2n  11607  m1expe  11632  m1exp1  11634  epttop  12298  neipsm  12362  tgioo  12754  sin0pilem2  12911  pilem3  12912  bj-nn0suc  13333  bj-nn0sucALT  13347  trirec0xor  13413