Theorem reximi 2647

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

Syntax hints:   -> wi 4   e. wcel 2209   E.wrex 2529

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-ial 1587

This theorem depends on definitions:  df-bi 117  df-ral 2533  df-rex 2534

This theorem is referenced by:  rexanaliim  2656  r19.29d2r  2695  r19.35-1  2701  r19.40  2705  reu3  3016  ssiun  4049  iinss  4059  elunirn  5962  tfrcllemssrecs  6613  nnawordex  6792  iinerm  6871  erovlem  6891  xpf1o  7134  fidcenumlemim  7259  omniwomnimkv  7497  genprndl  7878  genprndu  7879  appdiv0nq  7921  ltexprlemm  7957  recexsrlem  8131  rereceu  8246  recexre  8896  aprcl  8964  rexanre  11964  climi2  12032  climi0  12033  climcaucn  12095  prodmodclem2  12322  prodmodc  12323  gcdsupex  12712  gcdsupcl  12713  bezoutlemeu  12762  dfgcd3  12765  isnsgrp  13698  rhmdvdsr  14455  eltg2b  15078  lmcvg  15241  cnptoprest  15263  lmtopcnp  15274  txbas  15282  metrest  15530  elply2  15759  2sqlem7  16154  umgr2edg1  16364  umgr2edgneu  16367  bj-charfunbi  16751  bj-findis  16919