Theorem rexex 3096

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∃wex 1812   ∈ wcel 2147  ∃wrex 3090

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3091

This theorem is used by:  reu3  3688  rmo2i  3839  dffo5  7131  el2xpss  8075  nqerf  11045  supsrlem  11226  vdwmc2  17189  toprntopon  23276  loop1cycl  30777  umgr2cycllem  30779  umgr2cycl  30780  isch3  31876  19.9d2rf  33141  volfiniune  34946  bnj594  35625  bnj1371  35742  bnj1374  35744  acwer1prc  35865  srepdflem1  36098  dfrdg4  36906  bj-0nelsngl  38075  bj-ccinftydisj  38339  poimirlem25  38768  mblfinlem3  38782  mblfinlem4  38783  clsk3nimkb  45243  grumnudlem  45472  ismnushort  45488  uniclaxun  46182  stoweidlem57  47282