Theorem rexex 3203

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

Syntax hints:   → wi 4   ∧ wa 399  ∃wex 1781   ∈ wcel 2111  ∃wrex 3107

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

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-rex 3112

This theorem is referenced by:  reu3  3666  rmo2i  3817  dffo5  6847  nqerf  10341  supsrlem  10522  vdwmc2  16305  toprntopon  21530  isch3  29024  19.9d2rf  30242  volfiniune  31599  bnj594  32294  bnj1371  32411  bnj1374  32413  loop1cycl  32497  umgr2cycllem  32500  umgr2cycl  32501  dfrdg4  33525  bj-0nelsngl  34407  bj-ccinftydisj  34628  poimirlem25  35082  mblfinlem3  35096  mblfinlem4  35097  clsk3nimkb  40743  grumnudlem  40993  stoweidlem57  42699