Theorem rexlimiva 2645

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

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

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-i5r 1583

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-ral 2515  df-rex 2516

This theorem is referenced by:  unon  4609  reg2exmidlema  4632  ssfilem  7062  ssfilemd  7064  diffitest  7076  fival  7169  elfi2  7171  fi0  7174  djuss  7269  updjud  7281  enumct  7314  finnum  7387  dmaddpqlem  7597  nqpi  7598  nq0nn  7662  recexprlemm  7844  iswrd  11119  wrdf  11123  rexanuz  11566  r19.2uz  11571  maxleast  11791  fsum2dlemstep  12013  fisumcom2  12017  fprod2dlemstep  12201  fprodcom2fi  12205  0dvds  12390  even2n  12453  m1expe  12478  m1exp1  12480  modprm0  12845  gsumval2  13498  dfgrp2  13628  epttop  14833  neipsm  14897  tgioo  15297  sin0pilem2  15525  pilem3  15526  perfect  15744  clwwlkn1loopb  16290  bj-nn0suc  16610  bj-nn0sucALT  16624  trirec0xor  16700