Theorem reximi 2629

Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 18-Oct-1996.)

Hypothesis

Ref	Expression
reximi.1	|- ( ph -> ps )

Assertion

Ref	Expression
reximi	|- ( E. x e. A ph -> E. x e. A ps )

Proof of Theorem reximi

Step	Hyp	Ref	Expression
1		reximi.1	. . 3 |- ( ph -> ps )
2	1	a1i 9	. 2 |- ( x e. A -> ( ph -> ps ) )
3	2	reximia 2627	1 |- ( E. x e. A ph -> E. x e. A ps )

Syntax hints:   -> wi 4   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-ial 1582

This theorem depends on definitions:  df-bi 117  df-ral 2515  df-rex 2516

This theorem is referenced by:  rexanaliim  2638  r19.29d2r  2677  r19.35-1  2683  r19.40  2687  reu3  2996  ssiun  4012  iinss  4022  elunirn  5906  tfrcllemssrecs  6517  nnawordex  6696  iinerm  6775  erovlem  6795  xpf1o  7029  fidcenumlemim  7150  omniwomnimkv  7365  genprndl  7740  genprndu  7741  appdiv0nq  7783  ltexprlemm  7819  recexsrlem  7993  rereceu  8108  recexre  8757  aprcl  8825  rexanre  11780  climi2  11848  climi0  11849  climcaucn  11911  prodmodclem2  12137  prodmodc  12138  gcdsupex  12527  gcdsupcl  12528  bezoutlemeu  12577  dfgcd3  12580  isnsgrp  13488  rhmdvdsr  14188  eltg2b  14777  lmcvg  14940  cnptoprest  14962  lmtopcnp  14973  txbas  14981  metrest  15229  elply2  15458  2sqlem7  15849  umgr2edg1  16059  umgr2edgneu  16062  bj-charfunbi  16406  bj-findis  16574