Theorem rexlimiva 2582

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

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

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 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-i5r 1528

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-ral 2453  df-rex 2454

This theorem is referenced by:  unon  4495  reg2exmidlema  4518  ssfilem  6853  diffitest  6865  fival  6947  elfi2  6949  fi0  6952  djuss  7047  updjud  7059  enumct  7092  finnum  7160  dmaddpqlem  7339  nqpi  7340  nq0nn  7404  recexprlemm  7586  rexanuz  10952  r19.2uz  10957  maxleast  11177  fsum2dlemstep  11397  fisumcom2  11401  fprod2dlemstep  11585  fprodcom2fi  11589  0dvds  11773  even2n  11833  m1expe  11858  m1exp1  11860  modprm0  12208  dfgrp2  12732  epttop  12884  neipsm  12948  tgioo  13340  sin0pilem2  13497  pilem3  13498  bj-nn0suc  13999  bj-nn0sucALT  14013  trirec0xor  14077