Theorem rexex 3073

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

Syntax hints:   → wi 4   ∧ wa 394  ∃wex 1773   ∈ wcel 2098  ∃wrex 3067

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

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-rex 3068

This theorem is referenced by:  reu3  3724  rmo2i  3883  dffo5  7119  el2xpss  8047  nqerf  10961  supsrlem  11142  vdwmc2  16955  toprntopon  22847  isch3  31071  19.9d2rf  32290  volfiniune  33882  bnj594  34576  bnj1371  34693  bnj1374  34695  loop1cycl  34780  umgr2cycllem  34783  umgr2cycl  34784  dfrdg4  35580  bj-0nelsngl  36483  bj-ccinftydisj  36725  poimirlem25  37151  mblfinlem3  37165  mblfinlem4  37166  clsk3nimkb  43501  grumnudlem  43753  ismnushort  43769  stoweidlem57  45474