Theorem rexex 3242

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

Syntax hints:   → wi 4   ∧ wa 398  ∃wex 1780   ∈ wcel 2114  ∃wrex 3141

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

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-rex 3146

This theorem is referenced by:  reu3  3720  rmo2i  3873  dffo5  6872  nqerf  10354  supsrlem  10535  vdwmc2  16317  toprntopon  21535  isch3  29020  19.9d2rf  30237  volfiniune  31491  bnj594  32186  bnj1371  32303  bnj1374  32305  loop1cycl  32386  umgr2cycllem  32389  umgr2cycl  32390  dfrdg4  33414  bj-0nelsngl  34285  bj-ccinftydisj  34497  poimirlem25  34919  mblfinlem3  34933  mblfinlem4  34934  clsk3nimkb  40397  grumnudlem  40628  stoweidlem57  42349