Theorem rexex 3059

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1779   ∈ wcel 2109  ∃wrex 3053

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 3054

This theorem is referenced by:  reu3  3698  rmo2i  3851  dffo5  7076  el2xpss  8016  nqerf  10883  supsrlem  11064  vdwmc2  16950  toprntopon  22812  isch3  31170  19.9d2rf  32398  volfiniune  34220  bnj594  34902  bnj1371  35019  bnj1374  35021  loop1cycl  35124  umgr2cycllem  35127  umgr2cycl  35128  dfrdg4  35939  bj-0nelsngl  36959  bj-ccinftydisj  37201  poimirlem25  37639  mblfinlem3  37653  mblfinlem4  37654  clsk3nimkb  44029  grumnudlem  44274  ismnushort  44290  uniclaxun  44976  stoweidlem57  46055