Theorem rexex 3091

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

Syntax hints:   → wi 4   ∧ wa 399  ∃wex 1798   ∈ wcel 2141  ∃wrex 3085

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

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-rex 3086

This theorem is referenced by:  reu3  3689  rmo2i  3841  dffo5  7081  el2xpss  8014  nqerf  10885  supsrlem  11066  vdwmc2  16998  toprntopon  22965  isch3  31390  19.9d2rf  32616  volfiniune  34488  bnj594  35171  bnj1371  35288  bnj1374  35290  loop1cycl  35451  umgr2cycllem  35454  umgr2cycl  35455  dfrdg4  36265  bj-0nelsngl  37420  bj-ccinftydisj  37669  poimirlem25  38108  mblfinlem3  38122  mblfinlem4  38123  clsk3nimkb  44580  grumnudlem  44825  ismnushort  44841  uniclaxun  45526  stoweidlem57  46595