Theorem rexlimiva 2643

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

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

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-i5r 1581

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513  df-rex 2514

This theorem is referenced by:  unon  4603  reg2exmidlema  4626  ssfilem  7037  diffitest  7049  fival  7137  elfi2  7139  fi0  7142  djuss  7237  updjud  7249  enumct  7282  finnum  7355  dmaddpqlem  7564  nqpi  7565  nq0nn  7629  recexprlemm  7811  iswrd  11073  wrdf  11077  rexanuz  11499  r19.2uz  11504  maxleast  11724  fsum2dlemstep  11945  fisumcom2  11949  fprod2dlemstep  12133  fprodcom2fi  12137  0dvds  12322  even2n  12385  m1expe  12410  m1exp1  12412  modprm0  12777  gsumval2  13430  dfgrp2  13560  epttop  14764  neipsm  14828  tgioo  15228  sin0pilem2  15456  pilem3  15457  perfect  15675  bj-nn0suc  16327  bj-nn0sucALT  16341  trirec0xor  16413