Theorem rexex 3063

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

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

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 3058

This theorem is referenced by:  reu3  3682  rmo2i  3835  dffo5  7043  el2xpss  7975  nqerf  10828  supsrlem  11009  vdwmc2  16893  toprntopon  22841  isch3  31223  19.9d2rf  32450  volfiniune  34264  bnj594  34945  bnj1371  35062  bnj1374  35064  loop1cycl  35202  umgr2cycllem  35205  umgr2cycl  35206  dfrdg4  36016  bj-0nelsngl  37036  bj-ccinftydisj  37278  poimirlem25  37705  mblfinlem3  37719  mblfinlem4  37720  clsk3nimkb  44157  grumnudlem  44402  ismnushort  44418  uniclaxun  45103  stoweidlem57  46179