Theorem reximi 2574

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

Syntax hints:   → wi 4   ∈ wcel 2148  ∃wrex 2456

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-ial 1534

This theorem depends on definitions:  df-bi 117  df-ral 2460  df-rex 2461

This theorem is referenced by:  r19.29d2r  2621  r19.35-1  2627  r19.40  2631  reu3  2928  ssiun  3929  iinss  3939  elunirn  5767  tfrcllemssrecs  6353  nnawordex  6530  iinerm  6607  erovlem  6627  xpf1o  6844  fidcenumlemim  6951  omniwomnimkv  7165  genprndl  7520  genprndu  7521  appdiv0nq  7563  ltexprlemm  7599  recexsrlem  7773  rereceu  7888  recexre  8535  aprcl  8603  rexanre  11229  climi2  11296  climi0  11297  climcaucn  11359  prodmodclem2  11585  prodmodc  11586  gcdsupex  11958  gcdsupcl  11959  bezoutlemeu  12008  dfgcd3  12011  isnsgrp  12812  eltg2b  13557  lmcvg  13720  cnptoprest  13742  lmtopcnp  13753  txbas  13761  metrest  14009  2sqlem7  14471  bj-charfunbi  14566  bj-findis  14734