Theorem rexlimiva 2602

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

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

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-i5r 1546

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2473  df-rex 2474

This theorem is referenced by:  unon  4525  reg2exmidlema  4548  ssfilem  6893  diffitest  6905  fival  6988  elfi2  6990  fi0  6993  djuss  7088  updjud  7100  enumct  7133  finnum  7201  dmaddpqlem  7395  nqpi  7396  nq0nn  7460  recexprlemm  7642  rexanuz  11016  r19.2uz  11021  maxleast  11241  fsum2dlemstep  11461  fisumcom2  11465  fprod2dlemstep  11649  fprodcom2fi  11653  0dvds  11837  even2n  11898  m1expe  11923  m1exp1  11925  modprm0  12273  dfgrp2  12943  epttop  13993  neipsm  14057  tgioo  14449  sin0pilem2  14606  pilem3  14607  bj-nn0suc  15119  bj-nn0sucALT  15133  trirec0xor  15197