Theorem reximi 2591

Description: Inference quantifying both antecedent and consequent. (Contributed by NM, 18-Oct-1996.)

Hypothesis

Ref	Expression
reximi.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
reximi	⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)

Proof of Theorem reximi

Step	Hyp	Ref	Expression
1		reximi.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	a1i 9	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 → 𝜓))
3	2	reximia 2589	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2164  ∃wrex 2473

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-ial 1545

This theorem depends on definitions:  df-bi 117  df-ral 2477  df-rex 2478

This theorem is referenced by:  r19.29d2r  2638  r19.35-1  2644  r19.40  2648  reu3  2951  ssiun  3955  iinss  3965  elunirn  5810  tfrcllemssrecs  6407  nnawordex  6584  iinerm  6663  erovlem  6683  xpf1o  6902  fidcenumlemim  7013  omniwomnimkv  7228  genprndl  7583  genprndu  7584  appdiv0nq  7626  ltexprlemm  7662  recexsrlem  7836  rereceu  7951  recexre  8599  aprcl  8667  rexanre  11367  climi2  11434  climi0  11435  climcaucn  11497  prodmodclem2  11723  prodmodc  11724  gcdsupex  12097  gcdsupcl  12098  bezoutlemeu  12147  dfgcd3  12150  isnsgrp  12992  rhmdvdsr  13674  eltg2b  14233  lmcvg  14396  cnptoprest  14418  lmtopcnp  14429  txbas  14437  metrest  14685  elply2  14914  2sqlem7  15278  bj-charfunbi  15373  bj-findis  15541