Theorem reximi 2641

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

Syntax hints:   -> wi 4   e. wcel 2205   E.wrex 2523

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 2527  df-rex 2528

This theorem is referenced by:  rexanaliim  2650  r19.29d2r  2689  r19.35-1  2695  r19.40  2699  reu3  3010  ssiun  4038  iinss  4048  elunirn  5945  tfrcllemssrecs  6596  nnawordex  6775  iinerm  6854  erovlem  6874  xpf1o  7110  fidcenumlemim  7235  omniwomnimkv  7471  genprndl  7852  genprndu  7853  appdiv0nq  7895  ltexprlemm  7931  recexsrlem  8105  rereceu  8220  recexre  8869  aprcl  8937  rexanre  11930  climi2  11998  climi0  11999  climcaucn  12061  prodmodclem2  12288  prodmodc  12289  gcdsupex  12678  gcdsupcl  12679  bezoutlemeu  12728  dfgcd3  12731  isnsgrp  13669  rhmdvdsr  14420  eltg2b  15045  lmcvg  15208  cnptoprest  15230  lmtopcnp  15241  txbas  15249  metrest  15497  elply2  15726  2sqlem7  16120  umgr2edg1  16330  umgr2edgneu  16333  bj-charfunbi  16707  bj-findis  16875