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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1780   ∈ wcel 2113  ∃wrex 3060

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 3061

This theorem is referenced by:  reu3  3685  rmo2i  3838  dffo5  7049  el2xpss  7981  nqerf  10841  supsrlem  11022  vdwmc2  16907  toprntopon  22869  isch3  31316  19.9d2rf  32543  volfiniune  34387  bnj594  35068  bnj1371  35185  bnj1374  35187  loop1cycl  35331  umgr2cycllem  35334  umgr2cycl  35335  dfrdg4  36145  bj-0nelsngl  37172  bj-ccinftydisj  37414  poimirlem25  37842  mblfinlem3  37856  mblfinlem4  37857  clsk3nimkb  44277  grumnudlem  44522  ismnushort  44538  uniclaxun  45223  stoweidlem57  46297