Theorem reximi 2574

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

Syntax hints:   -> wi 4   e. wcel 2148   E.wrex 2456

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-ial 1534

This theorem depends on definitions:  df-bi 117  df-ral 2460  df-rex 2461

This theorem is referenced by:  r19.29d2r  2621  r19.35-1  2627  r19.40  2631  reu3  2927  ssiun  3928  iinss  3938  elunirn  5766  tfrcllemssrecs  6352  nnawordex  6529  iinerm  6606  erovlem  6626  xpf1o  6843  fidcenumlemim  6950  omniwomnimkv  7164  genprndl  7519  genprndu  7520  appdiv0nq  7562  ltexprlemm  7598  recexsrlem  7772  rereceu  7887  recexre  8534  aprcl  8602  rexanre  11228  climi2  11295  climi0  11296  climcaucn  11358  prodmodclem2  11584  prodmodc  11585  gcdsupex  11957  gcdsupcl  11958  bezoutlemeu  12007  dfgcd3  12010  isnsgrp  12811  eltg2b  13524  lmcvg  13687  cnptoprest  13709  lmtopcnp  13720  txbas  13728  metrest  13976  2sqlem7  14438  bj-charfunbi  14533  bj-findis  14701