Theorem reximi 2567

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

Syntax hints:   -> wi 4   e. wcel 2141   E.wrex 2449

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 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-ial 1527

This theorem depends on definitions:  df-bi 116  df-ral 2453  df-rex 2454

This theorem is referenced by:  r19.29d2r  2614  r19.35-1  2620  r19.40  2624  reu3  2920  ssiun  3915  iinss  3924  elunirn  5745  tfrcllemssrecs  6331  nnawordex  6508  iinerm  6585  erovlem  6605  xpf1o  6822  fidcenumlemim  6929  omniwomnimkv  7143  genprndl  7483  genprndu  7484  appdiv0nq  7526  ltexprlemm  7562  recexsrlem  7736  rereceu  7851  recexre  8497  aprcl  8565  rexanre  11184  climi2  11251  climi0  11252  climcaucn  11314  prodmodclem2  11540  prodmodc  11541  gcdsupex  11912  gcdsupcl  11913  bezoutlemeu  11962  dfgcd3  11965  isnsgrp  12647  eltg2b  12848  lmcvg  13011  cnptoprest  13033  lmtopcnp  13044  txbas  13052  metrest  13300  2sqlem7  13751  bj-charfunbi  13846  bj-findis  14014