Theorem rexex 3059

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

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

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 3054

This theorem is referenced by:  reu3  3689  rmo2i  3842  dffo5  7042  el2xpss  7979  nqerf  10843  supsrlem  11024  vdwmc2  16909  toprntopon  22828  isch3  31203  19.9d2rf  32431  volfiniune  34196  bnj594  34878  bnj1371  34995  bnj1374  34997  loop1cycl  35109  umgr2cycllem  35112  umgr2cycl  35113  dfrdg4  35924  bj-0nelsngl  36944  bj-ccinftydisj  37186  poimirlem25  37624  mblfinlem3  37638  mblfinlem4  37639  clsk3nimkb  44013  grumnudlem  44258  ismnushort  44274  uniclaxun  44960  stoweidlem57  46039