Theorem reximi 2529

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

Syntax hints:   -> wi 4   e. wcel 1480   E.wrex 2417

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-ial 1514

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

This theorem is referenced by:  r19.29d2r  2576  r19.35-1  2581  r19.40  2585  reu3  2874  ssiun  3855  iinss  3864  elunirn  5667  tfrcllemssrecs  6249  nnawordex  6424  iinerm  6501  erovlem  6521  xpf1o  6738  fidcenumlemim  6840  genprndl  7329  genprndu  7330  appdiv0nq  7372  ltexprlemm  7408  recexsrlem  7582  rereceu  7697  recexre  8340  aprcl  8408  rexanre  10992  climi2  11057  climi0  11058  climcaucn  11120  prodmodclem2  11346  prodmodc  11347  gcdsupex  11646  gcdsupcl  11647  bezoutlemeu  11695  dfgcd3  11698  eltg2b  12223  lmcvg  12386  cnptoprest  12408  lmtopcnp  12419  txbas  12427  metrest  12675  bj-findis  13177