Theorem rexex 3167

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 3069	. 2 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
2		exsimpr 1873	. 2 ⊢ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) → ∃𝑥𝜑)
3	1, 2	sylbi 216	1 ⊢ (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥𝜑)

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1783   ∈ wcel 2108  ∃wrex 3064

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-rex 3069

This theorem is referenced by:  reu3  3657  rmo2i  3817  dffo5  6962  nqerf  10617  supsrlem  10798  vdwmc2  16608  toprntopon  21982  isch3  29504  19.9d2rf  30721  volfiniune  32098  bnj594  32792  bnj1371  32909  bnj1374  32911  loop1cycl  32999  umgr2cycllem  33002  umgr2cycl  33003  elxpxpss  33587  dfrdg4  34180  bj-0nelsngl  35088  bj-ccinftydisj  35311  poimirlem25  35729  mblfinlem3  35743  mblfinlem4  35744  clsk3nimkb  41539  grumnudlem  41792  ismnushort  41808  stoweidlem57  43488