Theorem rexex 3098

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∃wex 1812   ∈ wcel 2146  ∃wrex 3092

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3093

This theorem is used by:  reu3  3693  rmo2i  3844  dffo5  7106  el2xpss  8043  nqerf  10933  supsrlem  11114  vdwmc2  17064  toprntopon  23119  isch3  31630  19.9d2rf  32853  volfiniune  34652  bnj594  35332  bnj1371  35449  bnj1374  35451  loop1cycl  35650  umgr2cycllem  35653  umgr2cycl  35654  dfrdg4  36464  bj-0nelsngl  37648  bj-ccinftydisj  37898  poimirlem25  38337  mblfinlem3  38351  mblfinlem4  38352  clsk3nimkb  44807  grumnudlem  45036  ismnushort  45052  uniclaxun  45736  stoweidlem57  46812