Theorem rexex 3095

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

Syntax hints:   → wi 4   ∧ wa 400  ∃wex 1809   ∈ wcel 2143  ∃wrex 3089

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-rex 3090

This theorem is referenced by:  reu3  3691  rmo2i  3842  dffo5  7101  el2xpss  8035  nqerf  10916  supsrlem  11097  vdwmc2  17040  toprntopon  23063  isch3  31571  19.9d2rf  32794  volfiniune  34598  bnj594  35278  bnj1371  35395  bnj1374  35397  loop1cycl  35607  umgr2cycllem  35610  umgr2cycl  35611  dfrdg4  36421  bj-0nelsngl  37585  bj-ccinftydisj  37835  poimirlem25  38274  mblfinlem3  38288  mblfinlem4  38289  clsk3nimkb  44746  grumnudlem  44975  ismnushort  44991  uniclaxun  45675  stoweidlem57  46751