Theorem reximi 2630

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

Syntax hints:   -> wi 4   e. wcel 2202   E.wrex 2512

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 2516  df-rex 2517

This theorem is referenced by:  rexanaliim  2639  r19.29d2r  2678  r19.35-1  2684  r19.40  2688  reu3  2997  ssiun  4017  iinss  4027  elunirn  5917  tfrcllemssrecs  6561  nnawordex  6740  iinerm  6819  erovlem  6839  xpf1o  7073  fidcenumlemim  7194  omniwomnimkv  7409  genprndl  7784  genprndu  7785  appdiv0nq  7827  ltexprlemm  7863  recexsrlem  8037  rereceu  8152  recexre  8800  aprcl  8868  rexanre  11843  climi2  11911  climi0  11912  climcaucn  11974  prodmodclem2  12201  prodmodc  12202  gcdsupex  12591  gcdsupcl  12592  bezoutlemeu  12641  dfgcd3  12644  isnsgrp  13552  rhmdvdsr  14253  eltg2b  14848  lmcvg  15011  cnptoprest  15033  lmtopcnp  15044  txbas  15052  metrest  15300  elply2  15529  2sqlem7  15923  umgr2edg1  16133  umgr2edgneu  16136  bj-charfunbi  16510  bj-findis  16678