Theorem rexex 3070

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

Syntax hints:   → wi 4   ∧ wa 396  ∃wex 1786   ∈ wcel 2119  ∃wrex 3064

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

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-rex 3065

This theorem is referenced by:  reu3  3675  rmo2i  3827  dffo5  7052  el2xpss  7986  nqerf  10851  supsrlem  11032  vdwmc2  16948  toprntopon  22915  isch3  31337  19.9d2rf  32563  volfiniune  34421  bnj594  35101  bnj1371  35218  bnj1374  35220  loop1cycl  35372  umgr2cycllem  35375  umgr2cycl  35376  dfrdg4  36186  bj-0nelsngl  37331  bj-ccinftydisj  37580  poimirlem25  38019  mblfinlem3  38033  mblfinlem4  38034  clsk3nimkb  44491  grumnudlem  44736  ismnushort  44752  uniclaxun  45437  stoweidlem57  46507