Theorem reximi 2607

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

Syntax hints:   → wi 4   ∈ wcel 2180  ∃wrex 2489

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 1473  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-4 1536  ax-ial 1560

This theorem depends on definitions:  df-bi 117  df-ral 2493  df-rex 2494

This theorem is referenced by:  rexanaliim  2616  r19.29d2r  2655  r19.35-1  2661  r19.40  2665  reu3  2973  ssiun  3986  iinss  3996  elunirn  5863  tfrcllemssrecs  6468  nnawordex  6645  iinerm  6724  erovlem  6744  xpf1o  6973  fidcenumlemim  7087  omniwomnimkv  7302  genprndl  7676  genprndu  7677  appdiv0nq  7719  ltexprlemm  7755  recexsrlem  7929  rereceu  8044  recexre  8693  aprcl  8761  rexanre  11697  climi2  11765  climi0  11766  climcaucn  11828  prodmodclem2  12054  prodmodc  12055  gcdsupex  12444  gcdsupcl  12445  bezoutlemeu  12494  dfgcd3  12497  isnsgrp  13405  rhmdvdsr  14104  eltg2b  14693  lmcvg  14856  cnptoprest  14878  lmtopcnp  14889  txbas  14897  metrest  15145  elply2  15374  2sqlem7  15765  umgr2edg1  15972  umgr2edgneu  15975  bj-charfunbi  16084  bj-findis  16252