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  4607  reg2exmidlema  4630  ssfilem  7057  diffitest  7069  fival  7160  elfi2  7162  fi0  7165  djuss  7260  updjud  7272  enumct  7305  finnum  7378  dmaddpqlem  7587  nqpi  7588  nq0nn  7652  recexprlemm  7834  iswrd  11105  wrdf  11109  rexanuz  11539  r19.2uz  11544  maxleast  11764  fsum2dlemstep  11985  fisumcom2  11989  fprod2dlemstep  12173  fprodcom2fi  12177  0dvds  12362  even2n  12425  m1expe  12450  m1exp1  12452  modprm0  12817  gsumval2  13470  dfgrp2  13600  epttop  14804  neipsm  14868  tgioo  15268  sin0pilem2  15496  pilem3  15497  perfect  15715  clwwlkn1loopb  16215  bj-nn0suc  16495  bj-nn0sucALT  16509  trirec0xor  16585