Theorem rexex 3095

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

Syntax hints:   → wi 4   ∧ wa 400  ∃wex 1802   ∈ wcel 2145  ∃wrex 3089

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-rex 3090

This theorem is referenced by:  reu3  3693  rmo2i  3844  dffo5  7089  el2xpss  8022  nqerf  10903  supsrlem  11084  vdwmc2  17029  toprntopon  23043  isch3  31502  19.9d2rf  32726  volfiniune  34537  bnj594  35217  bnj1371  35334  bnj1374  35336  loop1cycl  35500  umgr2cycllem  35503  umgr2cycl  35504  dfrdg4  36314  bj-0nelsngl  37468  bj-ccinftydisj  37717  poimirlem25  38156  mblfinlem3  38170  mblfinlem4  38171  clsk3nimkb  44628  grumnudlem  44859  ismnushort  44875  uniclaxun  45560  stoweidlem57  46629