Theorem rexex 3062

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1780   ∈ wcel 2111  ∃wrex 3056

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3057

This theorem is referenced by:  reu3  3686  rmo2i  3839  dffo5  7037  el2xpss  7969  nqerf  10818  supsrlem  10999  vdwmc2  16888  toprntopon  22838  isch3  31216  19.9d2rf  32443  volfiniune  34238  bnj594  34919  bnj1371  35036  bnj1374  35038  loop1cycl  35169  umgr2cycllem  35172  umgr2cycl  35173  dfrdg4  35984  bj-0nelsngl  37004  bj-ccinftydisj  37246  poimirlem25  37684  mblfinlem3  37698  mblfinlem4  37699  clsk3nimkb  44072  grumnudlem  44317  ismnushort  44333  uniclaxun  45018  stoweidlem57  46094