Theorem rexex 3073

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1775   ∈ wcel 2105  ∃wrex 3067

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-rex 3068

This theorem is referenced by:  reu3  3735  rmo2i  3896  dffo5  7123  el2xpss  8060  nqerf  10967  supsrlem  11148  vdwmc2  17012  toprntopon  22946  isch3  31269  19.9d2rf  32497  volfiniune  34210  bnj594  34904  bnj1371  35021  bnj1374  35023  loop1cycl  35121  umgr2cycllem  35124  umgr2cycl  35125  dfrdg4  35932  bj-0nelsngl  36953  bj-ccinftydisj  37195  poimirlem25  37631  mblfinlem3  37645  mblfinlem4  37646  clsk3nimkb  44029  grumnudlem  44280  ismnushort  44296  stoweidlem57  46012