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  3674  rmo2i  3827  dffo5  7050  el2xpss  7983  nqerf  10844  supsrlem  11025  vdwmc2  16941  toprntopon  22900  isch3  31327  19.9d2rf  32553  volfiniune  34390  bnj594  35070  bnj1371  35187  bnj1374  35189  loop1cycl  35335  umgr2cycllem  35338  umgr2cycl  35339  dfrdg4  36149  bj-0nelsngl  37294  bj-ccinftydisj  37543  poimirlem25  37980  mblfinlem3  37994  mblfinlem4  37995  clsk3nimkb  44485  grumnudlem  44730  ismnushort  44746  uniclaxun  45431  stoweidlem57  46503