Theorem rexex 3068

Description: Restricted existence implies existence. (Contributed by NM, 11-Nov-1995.)

Assertion

Ref	Expression
rexex	⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥𝜑)

Proof of Theorem rexex

Step	Hyp	Ref	Expression
1		df-rex 3063	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
2		exsimpr 1871	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥𝜑)
3	1, 2	sylbi 217	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥𝜑)

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1781   ∈ wcel 2114  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3063

This theorem is referenced by:  reu3  3687  rmo2i  3840  dffo5  7058  el2xpss  7991  nqerf  10853  supsrlem  11034  vdwmc2  16919  toprntopon  22881  isch3  31328  19.9d2rf  32554  volfiniune  34407  bnj594  35087  bnj1371  35204  bnj1374  35206  loop1cycl  35350  umgr2cycllem  35353  umgr2cycl  35354  dfrdg4  36164  bj-0nelsngl  37213  bj-ccinftydisj  37462  poimirlem25  37890  mblfinlem3  37904  mblfinlem4  37905  clsk3nimkb  44390  grumnudlem  44635  ismnushort  44651  uniclaxun  45336  stoweidlem57  46409