Theorem rexex 3067

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1781   ∈ wcel 2114  ∃wrex 3061

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3062

This theorem is referenced by:  reu3  3673  rmo2i  3826  dffo5  7056  el2xpss  7990  nqerf  10853  supsrlem  11034  vdwmc2  16950  toprntopon  22890  isch3  31312  19.9d2rf  32538  volfiniune  34374  bnj594  35054  bnj1371  35171  bnj1374  35173  loop1cycl  35319  umgr2cycllem  35322  umgr2cycl  35323  dfrdg4  36133  bj-0nelsngl  37278  bj-ccinftydisj  37527  poimirlem25  37966  mblfinlem3  37980  mblfinlem4  37981  clsk3nimkb  44467  grumnudlem  44712  ismnushort  44728  uniclaxun  45413  stoweidlem57  46485