Theorem rexlimiva 2663

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

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

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-i5r 1588

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533  df-rex 2534

This theorem is referenced by:  unon  4653  reg2exmidlema  4676  ssfilem  7167  ssfilemd  7169  diffitest  7181  fival  7294  elfi2  7296  fi0  7299  djuss  7400  updjud  7412  enumct  7445  finnum  7518  dmaddpqlem  7734  nqpi  7735  nq0nn  7799  recexprlemm  7981  iswrd  11284  wrdf  11288  rexanuz  11732  r19.2uz  11737  maxleast  11957  fsum2dlemstep  12179  fisumcom2  12183  fprod2dlemstep  12367  fprodcom2fi  12371  0dvds  12556  even2n  12619  m1expe  12644  m1exp1  12646  modprm0  13011  gzsumval2  13691  dfgrp2  13809  epttop  15114  neipsm  15178  tgioo  15578  sin0pilem2  15806  pilem3  15807  perfect  16029  clwwlkn1loopb  16575  bj-nn0suc  16904  bj-nn0sucALT  16918  trirec0xor  16999