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  4547  reg2exmidlema  4570  ssfilem  6936  diffitest  6948  fival  7036  elfi2  7038  fi0  7041  djuss  7136  updjud  7148  enumct  7181  finnum  7250  dmaddpqlem  7444  nqpi  7445  nq0nn  7509  recexprlemm  7691  iswrd  10937  wrdf  10941  rexanuz  11153  r19.2uz  11158  maxleast  11378  fsum2dlemstep  11599  fisumcom2  11603  fprod2dlemstep  11787  fprodcom2fi  11791  0dvds  11976  even2n  12039  m1expe  12064  m1exp1  12066  modprm0  12423  gsumval2  13040  dfgrp2  13159  epttop  14326  neipsm  14390  tgioo  14790  sin0pilem2  15018  pilem3  15019  perfect  15237  bj-nn0suc  15610  bj-nn0sucALT  15624  trirec0xor  15689