Theorem rexex 3060

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1779   ∈ wcel 2109  ∃wrex 3054

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3055

This theorem is referenced by:  reu3  3701  rmo2i  3854  dffo5  7079  el2xpss  8019  nqerf  10890  supsrlem  11071  vdwmc2  16957  toprntopon  22819  isch3  31177  19.9d2rf  32405  volfiniune  34227  bnj594  34909  bnj1371  35026  bnj1374  35028  loop1cycl  35131  umgr2cycllem  35134  umgr2cycl  35135  dfrdg4  35946  bj-0nelsngl  36966  bj-ccinftydisj  37208  poimirlem25  37646  mblfinlem3  37660  mblfinlem4  37661  clsk3nimkb  44036  grumnudlem  44281  ismnushort  44297  uniclaxun  44983  stoweidlem57  46062