Theorem rexlimiva 2618

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

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

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-i5r 1558

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-ral 2489  df-rex 2490

This theorem is referenced by:  unon  4560  reg2exmidlema  4583  ssfilem  6974  diffitest  6986  fival  7074  elfi2  7076  fi0  7079  djuss  7174  updjud  7186  enumct  7219  finnum  7292  dmaddpqlem  7492  nqpi  7493  nq0nn  7557  recexprlemm  7739  iswrd  10998  wrdf  11002  rexanuz  11332  r19.2uz  11337  maxleast  11557  fsum2dlemstep  11778  fisumcom2  11782  fprod2dlemstep  11966  fprodcom2fi  11970  0dvds  12155  even2n  12218  m1expe  12243  m1exp1  12245  modprm0  12610  gsumval2  13262  dfgrp2  13392  epttop  14595  neipsm  14659  tgioo  15059  sin0pilem2  15287  pilem3  15288  perfect  15506  bj-nn0suc  15937  bj-nn0sucALT  15951  trirec0xor  16021