Theorem rexex 3093

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

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

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 3088

This theorem is used by:  reu3  3685  rmo2i  3835  dffo5  7096  el2xpss  8037  nqerf  10996  supsrlem  11177  vdwmc2  17137  toprntopon  23223  loop1cycl  30726  umgr2cycllem  30728  umgr2cycl  30729  isch3  31825  19.9d2rf  33048  volfiniune  34845  bnj594  35525  bnj1371  35642  bnj1374  35644  dfrdg4  36685  bj-0nelsngl  37854  bj-ccinftydisj  38102  poimirlem25  38531  mblfinlem3  38545  mblfinlem4  38546  clsk3nimkb  44999  grumnudlem  45228  ismnushort  45244  uniclaxun  45928  stoweidlem57  47011