Theorem rexex 3170

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

Syntax hints:   → wi 4   ∧ wa 396  ∃wex 1786   ∈ wcel 2110  ∃wrex 3067

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1787  df-rex 3072

This theorem is referenced by:  reu3  3666  rmo2i  3826  dffo5  6977  nqerf  10697  supsrlem  10878  vdwmc2  16691  toprntopon  22085  isch3  29612  19.9d2rf  30829  volfiniune  32207  bnj594  32901  bnj1371  33018  bnj1374  33020  loop1cycl  33108  umgr2cycllem  33111  umgr2cycl  33112  elxpxpss  33693  dfrdg4  34262  bj-0nelsngl  35170  bj-ccinftydisj  35393  poimirlem25  35811  mblfinlem3  35825  mblfinlem4  35826  clsk3nimkb  41632  grumnudlem  41885  ismnushort  41901  stoweidlem57  43580