Theorem reximi 2563

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

Syntax hints:   → wi 4   ∈ wcel 2136  ∃wrex 2445

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 1435  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-ial 1522

This theorem depends on definitions:  df-bi 116  df-ral 2449  df-rex 2450

This theorem is referenced by:  r19.29d2r  2610  r19.35-1  2616  r19.40  2620  reu3  2916  ssiun  3908  iinss  3917  elunirn  5734  tfrcllemssrecs  6320  nnawordex  6496  iinerm  6573  erovlem  6593  xpf1o  6810  fidcenumlemim  6917  omniwomnimkv  7131  genprndl  7462  genprndu  7463  appdiv0nq  7505  ltexprlemm  7541  recexsrlem  7715  rereceu  7830  recexre  8476  aprcl  8544  rexanre  11162  climi2  11229  climi0  11230  climcaucn  11292  prodmodclem2  11518  prodmodc  11519  gcdsupex  11890  gcdsupcl  11891  bezoutlemeu  11940  dfgcd3  11943  eltg2b  12694  lmcvg  12857  cnptoprest  12879  lmtopcnp  12890  txbas  12898  metrest  13146  2sqlem7  13597  bj-charfunbi  13693  bj-findis  13861