Theorem reximi 2561

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 2559	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∈ wcel 2135  ∃wrex 2443

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 1434  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-4 1497  ax-ial 1521

This theorem depends on definitions:  df-bi 116  df-ral 2447  df-rex 2448

This theorem is referenced by:  r19.29d2r  2608  r19.35-1  2614  r19.40  2618  reu3  2911  ssiun  3902  iinss  3911  elunirn  5728  tfrcllemssrecs  6311  nnawordex  6487  iinerm  6564  erovlem  6584  xpf1o  6801  fidcenumlemim  6908  omniwomnimkv  7122  genprndl  7453  genprndu  7454  appdiv0nq  7496  ltexprlemm  7532  recexsrlem  7706  rereceu  7821  recexre  8467  aprcl  8535  rexanre  11148  climi2  11215  climi0  11216  climcaucn  11278  prodmodclem2  11504  prodmodc  11505  gcdsupex  11875  gcdsupcl  11876  bezoutlemeu  11925  dfgcd3  11928  eltg2b  12595  lmcvg  12758  cnptoprest  12780  lmtopcnp  12791  txbas  12799  metrest  13047  bj-charfunbi  13528  bj-findis  13696