Theorem reximi 2602

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

Syntax hints:   -> wi 4   e. wcel 2175   E.wrex 2484

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 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-ial 1556

This theorem depends on definitions:  df-bi 117  df-ral 2488  df-rex 2489

This theorem is referenced by:  r19.29d2r  2649  r19.35-1  2655  r19.40  2659  reu3  2962  ssiun  3968  iinss  3978  elunirn  5834  tfrcllemssrecs  6437  nnawordex  6614  iinerm  6693  erovlem  6713  xpf1o  6940  fidcenumlemim  7053  omniwomnimkv  7268  genprndl  7633  genprndu  7634  appdiv0nq  7676  ltexprlemm  7712  recexsrlem  7886  rereceu  8001  recexre  8650  aprcl  8718  rexanre  11473  climi2  11541  climi0  11542  climcaucn  11604  prodmodclem2  11830  prodmodc  11831  gcdsupex  12220  gcdsupcl  12221  bezoutlemeu  12270  dfgcd3  12273  isnsgrp  13180  rhmdvdsr  13879  eltg2b  14468  lmcvg  14631  cnptoprest  14653  lmtopcnp  14664  txbas  14672  metrest  14920  elply2  15149  2sqlem7  15540  bj-charfunbi  15680  bj-findis  15848