Theorem reximi 2639

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

Syntax hints:   → wi 4   ∈ wcel 2203  ∃wrex 2521

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 2525  df-rex 2526

This theorem is referenced by:  rexanaliim  2648  r19.29d2r  2687  r19.35-1  2693  r19.40  2697  reu3  3006  ssiun  4032  iinss  4042  elunirn  5938  tfrcllemssrecs  6582  nnawordex  6761  iinerm  6840  erovlem  6860  xpf1o  7096  fidcenumlemim  7221  omniwomnimkv  7457  genprndl  7832  genprndu  7833  appdiv0nq  7875  ltexprlemm  7911  recexsrlem  8085  rereceu  8200  recexre  8848  aprcl  8916  rexanre  11898  climi2  11966  climi0  11967  climcaucn  12029  prodmodclem2  12256  prodmodc  12257  gcdsupex  12646  gcdsupcl  12647  bezoutlemeu  12696  dfgcd3  12699  isnsgrp  13608  rhmdvdsr  14309  eltg2b  14906  lmcvg  15069  cnptoprest  15091  lmtopcnp  15102  txbas  15110  metrest  15358  elply2  15587  2sqlem7  15981  umgr2edg1  16191  umgr2edgneu  16194  bj-charfunbi  16568  bj-findis  16736