Theorem reximi 2627

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

Syntax hints:   → wi 4   ∈ wcel 2200  ∃wrex 2509

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-ial 1580

This theorem depends on definitions:  df-bi 117  df-ral 2513  df-rex 2514

This theorem is referenced by:  rexanaliim  2636  r19.29d2r  2675  r19.35-1  2681  r19.40  2685  reu3  2994  ssiun  4010  iinss  4020  elunirn  5902  tfrcllemssrecs  6513  nnawordex  6692  iinerm  6771  erovlem  6791  xpf1o  7025  fidcenumlemim  7145  omniwomnimkv  7360  genprndl  7734  genprndu  7735  appdiv0nq  7777  ltexprlemm  7813  recexsrlem  7987  rereceu  8102  recexre  8751  aprcl  8819  rexanre  11774  climi2  11842  climi0  11843  climcaucn  11905  prodmodclem2  12131  prodmodc  12132  gcdsupex  12521  gcdsupcl  12522  bezoutlemeu  12571  dfgcd3  12574  isnsgrp  13482  rhmdvdsr  14182  eltg2b  14771  lmcvg  14934  cnptoprest  14956  lmtopcnp  14967  txbas  14975  metrest  15223  elply2  15452  2sqlem7  15843  umgr2edg1  16053  umgr2edgneu  16056  bj-charfunbi  16356  bj-findis  16524