Theorem reximi 2574

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

Syntax hints:   → wi 4   ∈ wcel 2148  ∃wrex 2456

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-ial 1534

This theorem depends on definitions:  df-bi 117  df-ral 2460  df-rex 2461

This theorem is referenced by:  r19.29d2r  2621  r19.35-1  2627  r19.40  2631  reu3  2929  ssiun  3930  iinss  3940  elunirn  5769  tfrcllemssrecs  6355  nnawordex  6532  iinerm  6609  erovlem  6629  xpf1o  6846  fidcenumlemim  6953  omniwomnimkv  7167  genprndl  7522  genprndu  7523  appdiv0nq  7565  ltexprlemm  7601  recexsrlem  7775  rereceu  7890  recexre  8537  aprcl  8605  rexanre  11231  climi2  11298  climi0  11299  climcaucn  11361  prodmodclem2  11587  prodmodc  11588  gcdsupex  11960  gcdsupcl  11961  bezoutlemeu  12010  dfgcd3  12013  isnsgrp  12817  eltg2b  13639  lmcvg  13802  cnptoprest  13824  lmtopcnp  13835  txbas  13843  metrest  14091  2sqlem7  14553  bj-charfunbi  14648  bj-findis  14816