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  7061  ssfilemd  7063  diffitest  7075  fival  7168  elfi2  7170  fi0  7173  djuss  7268  updjud  7280  enumct  7313  finnum  7386  dmaddpqlem  7596  nqpi  7597  nq0nn  7661  recexprlemm  7843  iswrd  11114  wrdf  11118  rexanuz  11548  r19.2uz  11553  maxleast  11773  fsum2dlemstep  11994  fisumcom2  11998  fprod2dlemstep  12182  fprodcom2fi  12186  0dvds  12371  even2n  12434  m1expe  12459  m1exp1  12461  modprm0  12826  gsumval2  13479  dfgrp2  13609  epttop  14813  neipsm  14877  tgioo  15277  sin0pilem2  15505  pilem3  15506  perfect  15724  clwwlkn1loopb  16270  bj-nn0suc  16559  bj-nn0sucALT  16573  trirec0xor  16649