Theorem rexex 3082

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1777   ∈ wcel 2108  ∃wrex 3076

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-rex 3077

This theorem is referenced by:  reu3  3749  rmo2i  3910  dffo5  7138  el2xpss  8078  nqerf  10999  supsrlem  11180  vdwmc2  17026  toprntopon  22952  isch3  31273  19.9d2rf  32498  volfiniune  34194  bnj594  34888  bnj1371  35005  bnj1374  35007  loop1cycl  35105  umgr2cycllem  35108  umgr2cycl  35109  dfrdg4  35915  bj-0nelsngl  36937  bj-ccinftydisj  37179  poimirlem25  37605  mblfinlem3  37619  mblfinlem4  37620  clsk3nimkb  44002  grumnudlem  44254  ismnushort  44270  stoweidlem57  45978