Theorem reximi 2647

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

Syntax hints:   → wi 4   ∈ wcel 2209  ∃wrex 2529

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-ial 1587

This theorem depends on definitions:  df-bi 117  df-ral 2533  df-rex 2534

This theorem is referenced by:  rexanaliim  2656  r19.29d2r  2695  r19.35-1  2701  r19.40  2705  reu3  3016  ssiun  4052  iinss  4062  elunirn  5966  tfrcllemssrecs  6617  nnawordex  6796  iinerm  6875  erovlem  6895  xpf1o  7138  fidcenumlemim  7263  omniwomnimkv  7501  genprndl  7882  genprndu  7883  appdiv0nq  7925  ltexprlemm  7961  recexsrlem  8135  rereceu  8250  recexre  8900  aprcl  8968  rexanre  11969  climi2  12037  climi0  12038  climcaucn  12100  prodmodclem2  12327  prodmodc  12328  gcdsupex  12717  gcdsupcl  12718  bezoutlemeu  12767  dfgcd3  12770  isnsgrp  13704  rhmdvdsr  14465  eltg2b  15138  lmcvg  15301  cnptoprest  15323  lmtopcnp  15334  txbas  15342  metrest  15590  elply2  15819  2sqlem7  16223  umgr2edg1  16433  umgr2edgneu  16436  bj-charfunbi  16820  bj-findis  16988