Theorem rexlimiva 2646

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

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

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-i5r 1584

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2516  df-rex 2517

This theorem is referenced by:  unon  4615  reg2exmidlema  4638  ssfilem  7105  ssfilemd  7107  diffitest  7119  fival  7229  elfi2  7231  fi0  7234  djuss  7329  updjud  7341  enumct  7374  finnum  7447  dmaddpqlem  7657  nqpi  7658  nq0nn  7722  recexprlemm  7904  iswrd  11181  wrdf  11185  rexanuz  11628  r19.2uz  11633  maxleast  11853  fsum2dlemstep  12075  fisumcom2  12079  fprod2dlemstep  12263  fprodcom2fi  12267  0dvds  12452  even2n  12515  m1expe  12540  m1exp1  12542  modprm0  12907  gsumval2  13560  dfgrp2  13690  epttop  14901  neipsm  14965  tgioo  15365  sin0pilem2  15593  pilem3  15594  perfect  15815  clwwlkn1loopb  16361  bj-nn0suc  16680  bj-nn0sucALT  16694  trirec0xor  16777