Theorem rexlimiva 2606

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

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

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 2477  df-rex 2478

This theorem is referenced by:  unon  4543  reg2exmidlema  4566  ssfilem  6931  diffitest  6943  fival  7029  elfi2  7031  fi0  7034  djuss  7129  updjud  7141  enumct  7174  finnum  7243  dmaddpqlem  7437  nqpi  7438  nq0nn  7502  recexprlemm  7684  iswrd  10916  wrdf  10920  rexanuz  11132  r19.2uz  11137  maxleast  11357  fsum2dlemstep  11577  fisumcom2  11581  fprod2dlemstep  11765  fprodcom2fi  11769  0dvds  11954  even2n  12015  m1expe  12040  m1exp1  12042  modprm0  12392  gsumval2  12980  dfgrp2  13099  epttop  14258  neipsm  14322  tgioo  14714  sin0pilem2  14917  pilem3  14918  bj-nn0suc  15456  bj-nn0sucALT  15470  trirec0xor  15535