Theorem reximi 2604

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

Syntax hints:   -> wi 4   e. wcel 2177   E.wrex 2486

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-ial 1558

This theorem depends on definitions:  df-bi 117  df-ral 2490  df-rex 2491

This theorem is referenced by:  r19.29d2r  2651  r19.35-1  2657  r19.40  2661  reu3  2967  ssiun  3975  iinss  3985  elunirn  5848  tfrcllemssrecs  6451  nnawordex  6628  iinerm  6707  erovlem  6727  xpf1o  6956  fidcenumlemim  7069  omniwomnimkv  7284  genprndl  7654  genprndu  7655  appdiv0nq  7697  ltexprlemm  7733  recexsrlem  7907  rereceu  8022  recexre  8671  aprcl  8739  rexanre  11606  climi2  11674  climi0  11675  climcaucn  11737  prodmodclem2  11963  prodmodc  11964  gcdsupex  12353  gcdsupcl  12354  bezoutlemeu  12403  dfgcd3  12406  isnsgrp  13313  rhmdvdsr  14012  eltg2b  14601  lmcvg  14764  cnptoprest  14786  lmtopcnp  14797  txbas  14805  metrest  15053  elply2  15282  2sqlem7  15673  bj-charfunbi  15885  bj-findis  16053