Theorem reximi 2639

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

Syntax hints:   -> wi 4   e. wcel 2203   E.wrex 2521

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-ial 1583

This theorem depends on definitions:  df-bi 117  df-ral 2525  df-rex 2526

This theorem is referenced by:  rexanaliim  2648  r19.29d2r  2687  r19.35-1  2693  r19.40  2697  reu3  3007  ssiun  4033  iinss  4043  elunirn  5939  tfrcllemssrecs  6583  nnawordex  6762  iinerm  6841  erovlem  6861  xpf1o  7097  fidcenumlemim  7222  omniwomnimkv  7458  genprndl  7836  genprndu  7837  appdiv0nq  7879  ltexprlemm  7915  recexsrlem  8089  rereceu  8204  recexre  8852  aprcl  8920  rexanre  11905  climi2  11973  climi0  11974  climcaucn  12036  prodmodclem2  12263  prodmodc  12264  gcdsupex  12653  gcdsupcl  12654  bezoutlemeu  12703  dfgcd3  12706  isnsgrp  13619  rhmdvdsr  14320  eltg2b  14919  lmcvg  15082  cnptoprest  15104  lmtopcnp  15115  txbas  15123  metrest  15371  elply2  15600  2sqlem7  15994  umgr2edg1  16204  umgr2edgneu  16207  bj-charfunbi  16581  bj-findis  16749