Theorem rexex 3066

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1779   ∈ wcel 2108  ∃wrex 3060

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3061

This theorem is referenced by:  reu3  3710  rmo2i  3863  dffo5  7093  el2xpss  8034  nqerf  10942  supsrlem  11123  vdwmc2  16997  toprntopon  22861  isch3  31168  19.9d2rf  32396  volfiniune  34207  bnj594  34889  bnj1371  35006  bnj1374  35008  loop1cycl  35105  umgr2cycllem  35108  umgr2cycl  35109  dfrdg4  35915  bj-0nelsngl  36935  bj-ccinftydisj  37177  poimirlem25  37615  mblfinlem3  37629  mblfinlem4  37630  clsk3nimkb  44011  grumnudlem  44257  ismnushort  44273  uniclaxun  44959  stoweidlem57  46034