Theorem rexex 3092

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∃wex 1811   ∈ wcel 2144  ∃wrex 3086

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

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-rex 3087

This theorem is used by:  reu3  3684  rmo2i  3834  dffo5  7104  el2xpss  8048  nqerf  11018  supsrlem  11199  vdwmc2  17162  toprntopon  23248  loop1cycl  30749  umgr2cycllem  30751  umgr2cycl  30752  isch3  31848  19.9d2rf  33113  volfiniune  34909  bnj594  35588  bnj1371  35705  bnj1374  35707  acwer1prc  35816  srepdflem1  36004  dfrdg4  36807  bj-0nelsngl  37976  bj-ccinftydisj  38227  poimirlem25  38656  mblfinlem3  38670  mblfinlem4  38671  clsk3nimkb  45133  grumnudlem  45362  ismnushort  45378  uniclaxun  46069  stoweidlem57  47160