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  4602  reg2exmidlema  4625  ssfilem  7033  diffitest  7045  fival  7133  elfi2  7135  fi0  7138  djuss  7233  updjud  7245  enumct  7278  finnum  7351  dmaddpqlem  7560  nqpi  7561  nq0nn  7625  recexprlemm  7807  iswrd  11068  wrdf  11072  rexanuz  11494  r19.2uz  11499  maxleast  11719  fsum2dlemstep  11940  fisumcom2  11944  fprod2dlemstep  12128  fprodcom2fi  12132  0dvds  12317  even2n  12380  m1expe  12405  m1exp1  12407  modprm0  12772  gsumval2  13425  dfgrp2  13555  epttop  14758  neipsm  14822  tgioo  15222  sin0pilem2  15450  pilem3  15451  perfect  15669  bj-nn0suc  16285  bj-nn0sucALT  16299  trirec0xor  16372