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  3009  ssiun  4035  iinss  4045  elunirn  5941  tfrcllemssrecs  6585  nnawordex  6764  iinerm  6843  erovlem  6863  xpf1o  7099  fidcenumlemim  7224  omniwomnimkv  7460  genprndl  7841  genprndu  7842  appdiv0nq  7884  ltexprlemm  7920  recexsrlem  8094  rereceu  8209  recexre  8857  aprcl  8925  rexanre  11913  climi2  11981  climi0  11982  climcaucn  12044  prodmodclem2  12271  prodmodc  12272  gcdsupex  12661  gcdsupcl  12662  bezoutlemeu  12711  dfgcd3  12714  isnsgrp  13640  rhmdvdsr  14342  eltg2b  14968  lmcvg  15131  cnptoprest  15153  lmtopcnp  15164  txbas  15172  metrest  15420  elply2  15649  2sqlem7  16043  umgr2edg1  16253  umgr2edgneu  16256  bj-charfunbi  16630  bj-findis  16798