Theorem reximi 2567

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

Syntax hints:   → wi 4   ∈ wcel 2141  ∃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  3913  iinss  3922  elunirn  5742  tfrcllemssrecs  6328  nnawordex  6504  iinerm  6581  erovlem  6601  xpf1o  6818  fidcenumlemim  6925  omniwomnimkv  7139  genprndl  7470  genprndu  7471  appdiv0nq  7513  ltexprlemm  7549  recexsrlem  7723  rereceu  7838  recexre  8484  aprcl  8552  rexanre  11171  climi2  11238  climi0  11239  climcaucn  11301  prodmodclem2  11527  prodmodc  11528  gcdsupex  11899  gcdsupcl  11900  bezoutlemeu  11949  dfgcd3  11952  isnsgrp  12634  eltg2b  12807  lmcvg  12970  cnptoprest  12992  lmtopcnp  13003  txbas  13011  metrest  13259  2sqlem7  13710  bj-charfunbi  13806  bj-findis  13974