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  5907  tfrcllemssrecs  6518  nnawordex  6697  iinerm  6776  erovlem  6796  xpf1o  7030  fidcenumlemim  7151  omniwomnimkv  7366  genprndl  7741  genprndu  7742  appdiv0nq  7784  ltexprlemm  7820  recexsrlem  7994  rereceu  8109  recexre  8758  aprcl  8826  rexanre  11798  climi2  11866  climi0  11867  climcaucn  11929  prodmodclem2  12156  prodmodc  12157  gcdsupex  12546  gcdsupcl  12547  bezoutlemeu  12596  dfgcd3  12599  isnsgrp  13507  rhmdvdsr  14208  eltg2b  14797  lmcvg  14960  cnptoprest  14982  lmtopcnp  14993  txbas  15001  metrest  15249  elply2  15478  2sqlem7  15869  umgr2edg1  16079  umgr2edgneu  16082  bj-charfunbi  16457  bj-findis  16625