Theorem reximi 2532

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

Syntax hints:   -> wi 4   e. wcel 1481   E.wrex 2418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-ial 1515

This theorem depends on definitions:  df-bi 116  df-ral 2422  df-rex 2423

This theorem is referenced by:  r19.29d2r  2579  r19.35-1  2584  r19.40  2588  reu3  2878  ssiun  3863  iinss  3872  elunirn  5675  tfrcllemssrecs  6257  nnawordex  6432  iinerm  6509  erovlem  6529  xpf1o  6746  fidcenumlemim  6848  omniwomnimkv  7049  genprndl  7353  genprndu  7354  appdiv0nq  7396  ltexprlemm  7432  recexsrlem  7606  rereceu  7721  recexre  8364  aprcl  8432  rexanre  11024  climi2  11089  climi0  11090  climcaucn  11152  prodmodclem2  11378  prodmodc  11379  gcdsupex  11682  gcdsupcl  11683  bezoutlemeu  11731  dfgcd3  11734  eltg2b  12262  lmcvg  12425  cnptoprest  12447  lmtopcnp  12458  txbas  12466  metrest  12714  bj-findis  13348