Theorem reximi 2594

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

Syntax hints:   → wi 4   ∈ wcel 2167  ∃wrex 2476

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-ial 1548

This theorem depends on definitions:  df-bi 117  df-ral 2480  df-rex 2481

This theorem is referenced by:  r19.29d2r  2641  r19.35-1  2647  r19.40  2651  reu3  2954  ssiun  3959  iinss  3969  elunirn  5816  tfrcllemssrecs  6419  nnawordex  6596  iinerm  6675  erovlem  6695  xpf1o  6914  fidcenumlemim  7027  omniwomnimkv  7242  genprndl  7607  genprndu  7608  appdiv0nq  7650  ltexprlemm  7686  recexsrlem  7860  rereceu  7975  recexre  8624  aprcl  8692  rexanre  11404  climi2  11472  climi0  11473  climcaucn  11535  prodmodclem2  11761  prodmodc  11762  gcdsupex  12151  gcdsupcl  12152  bezoutlemeu  12201  dfgcd3  12204  isnsgrp  13110  rhmdvdsr  13809  eltg2b  14398  lmcvg  14561  cnptoprest  14583  lmtopcnp  14594  txbas  14602  metrest  14850  elply2  15079  2sqlem7  15470  bj-charfunbi  15565  bj-findis  15733