Theorem rexex 3094

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

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

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 3089

This theorem is used by:  reu3  3688  rmo2i  3838  dffo5  7101  el2xpss  8038  nqerf  10943  supsrlem  11124  vdwmc2  17077  toprntopon  23156  loop1cycl  30631  umgr2cycllem  30633  umgr2cycl  30634  isch3  31730  19.9d2rf  32953  volfiniune  34749  bnj594  35429  bnj1371  35546  bnj1374  35548  dfrdg4  36538  bj-0nelsngl  37723  bj-ccinftydisj  37973  poimirlem25  38402  mblfinlem3  38416  mblfinlem4  38417  clsk3nimkb  44888  grumnudlem  45117  ismnushort  45133  uniclaxun  45817  stoweidlem57  46893