Theorem rexlimiva 2609

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

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

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-i5r 1549

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-ral 2480  df-rex 2481

This theorem is referenced by:  unon  4548  reg2exmidlema  4571  ssfilem  6945  diffitest  6957  fival  7045  elfi2  7047  fi0  7050  djuss  7145  updjud  7157  enumct  7190  finnum  7261  dmaddpqlem  7461  nqpi  7462  nq0nn  7526  recexprlemm  7708  iswrd  10954  wrdf  10958  rexanuz  11170  r19.2uz  11175  maxleast  11395  fsum2dlemstep  11616  fisumcom2  11620  fprod2dlemstep  11804  fprodcom2fi  11808  0dvds  11993  even2n  12056  m1expe  12081  m1exp1  12083  modprm0  12448  gsumval2  13099  dfgrp2  13229  epttop  14410  neipsm  14474  tgioo  14874  sin0pilem2  15102  pilem3  15103  perfect  15321  bj-nn0suc  15694  bj-nn0sucALT  15708  trirec0xor  15776