Theorem reximi 2587

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

Syntax hints:   -> wi 4   e. wcel 2160   E.wrex 2469

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-ial 1545

This theorem depends on definitions:  df-bi 117  df-ral 2473  df-rex 2474

This theorem is referenced by:  r19.29d2r  2634  r19.35-1  2640  r19.40  2644  reu3  2942  ssiun  3943  iinss  3953  elunirn  5783  tfrcllemssrecs  6371  nnawordex  6548  iinerm  6625  erovlem  6645  xpf1o  6862  fidcenumlemim  6969  omniwomnimkv  7183  genprndl  7538  genprndu  7539  appdiv0nq  7581  ltexprlemm  7617  recexsrlem  7791  rereceu  7906  recexre  8553  aprcl  8621  rexanre  11247  climi2  11314  climi0  11315  climcaucn  11377  prodmodclem2  11603  prodmodc  11604  gcdsupex  11976  gcdsupcl  11977  bezoutlemeu  12026  dfgcd3  12029  isnsgrp  12835  rhmdvdsr  13486  eltg2b  13938  lmcvg  14101  cnptoprest  14123  lmtopcnp  14134  txbas  14142  metrest  14390  2sqlem7  14852  bj-charfunbi  14947  bj-findis  15115