Theorem rexex 3182

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

Syntax hints:   → wi 4   ∧ wa 386  ∃wex 1823   ∈ wcel 2106  ∃wrex 3090

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

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-rex 3095

This theorem is referenced by:  reu3  3607  rmo2i  3743  dffo5  6640  nqerf  10087  supsrlem  10268  vdwmc2  16087  toprntopon  21137  clwlkclwwlkfOLD  27392  isch3  28684  19.9d2rf  29904  volfiniune  30905  bnj594  31595  bnj1371  31710  bnj1374  31712  dfrdg4  32661  bj-0nelsngl  33545  bj-ccinftydisj  33704  poimirlem25  34054  mblfinlem3  34068  mblfinlem4  34069  clsk3nimkb  39286  stoweidlem57  41193