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  4039  iinss  4049  elunirn  5947  tfrcllemssrecs  6598  nnawordex  6777  iinerm  6856  erovlem  6876  xpf1o  7112  fidcenumlemim  7237  omniwomnimkv  7473  genprndl  7854  genprndu  7855  appdiv0nq  7897  ltexprlemm  7933  recexsrlem  8107  rereceu  8222  recexre  8872  aprcl  8940  rexanre  11936  climi2  12004  climi0  12005  climcaucn  12067  prodmodclem2  12294  prodmodc  12295  gcdsupex  12684  gcdsupcl  12685  bezoutlemeu  12734  dfgcd3  12737  isnsgrp  13670  rhmdvdsr  14427  eltg2b  15050  lmcvg  15213  cnptoprest  15235  lmtopcnp  15246  txbas  15254  metrest  15502  elply2  15731  2sqlem7  16125  umgr2edg1  16335  umgr2edgneu  16338  bj-charfunbi  16722  bj-findis  16890