Theorem rexex 3171

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

Syntax hints:   → wi 4   ∧ wa 396  ∃wex 1782   ∈ wcel 2106  ∃wrex 3065

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-rex 3070

This theorem is referenced by:  reu3  3662  rmo2i  3821  dffo5  6980  nqerf  10686  supsrlem  10867  vdwmc2  16680  toprntopon  22074  isch3  29603  19.9d2rf  30820  volfiniune  32198  bnj594  32892  bnj1371  33009  bnj1374  33011  loop1cycl  33099  umgr2cycllem  33102  umgr2cycl  33103  elxpxpss  33684  dfrdg4  34253  bj-0nelsngl  35161  bj-ccinftydisj  35384  poimirlem25  35802  mblfinlem3  35816  mblfinlem4  35817  clsk3nimkb  41650  grumnudlem  41903  ismnushort  41919  stoweidlem57  43598