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  11502  climi2  11570  climi0  11571  climcaucn  11633  prodmodclem2  11859  prodmodc  11860  gcdsupex  12249  gcdsupcl  12250  bezoutlemeu  12299  dfgcd3  12302  isnsgrp  13209  rhmdvdsr  13908  eltg2b  14497  lmcvg  14660  cnptoprest  14682  lmtopcnp  14693  txbas  14701  metrest  14949  elply2  15178  2sqlem7  15569  bj-charfunbi  15709  bj-findis  15877