Theorem reximi 2641

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

Syntax hints:   → wi 4   ∈ wcel 2205  ∃wrex 2523

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-ial 1583

This theorem depends on definitions:  df-bi 117  df-ral 2527  df-rex 2528

This theorem is referenced by:  rexanaliim  2650  r19.29d2r  2689  r19.35-1  2695  r19.40  2699  reu3  3010  ssiun  4038  iinss  4048  elunirn  5945  tfrcllemssrecs  6596  nnawordex  6775  iinerm  6854  erovlem  6874  xpf1o  7110  fidcenumlemim  7235  omniwomnimkv  7471  genprndl  7852  genprndu  7853  appdiv0nq  7895  ltexprlemm  7931  recexsrlem  8105  rereceu  8220  recexre  8870  aprcl  8938  rexanre  11933  climi2  12001  climi0  12002  climcaucn  12064  prodmodclem2  12291  prodmodc  12292  gcdsupex  12681  gcdsupcl  12682  bezoutlemeu  12731  dfgcd3  12734  isnsgrp  13672  rhmdvdsr  14423  eltg2b  15048  lmcvg  15211  cnptoprest  15233  lmtopcnp  15244  txbas  15252  metrest  15500  elply2  15729  2sqlem7  16123  umgr2edg1  16333  umgr2edgneu  16336  bj-charfunbi  16720  bj-findis  16888