Theorem rexex 3076

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1779   ∈ wcel 2108  ∃wrex 3070

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3071

This theorem is referenced by:  reu3  3733  rmo2i  3888  dffo5  7124  el2xpss  8062  nqerf  10970  supsrlem  11151  vdwmc2  17017  toprntopon  22931  isch3  31260  19.9d2rf  32488  volfiniune  34231  bnj594  34926  bnj1371  35043  bnj1374  35045  loop1cycl  35142  umgr2cycllem  35145  umgr2cycl  35146  dfrdg4  35952  bj-0nelsngl  36972  bj-ccinftydisj  37214  poimirlem25  37652  mblfinlem3  37666  mblfinlem4  37667  clsk3nimkb  44053  grumnudlem  44304  ismnushort  44320  uniclaxun  45003  stoweidlem57  46072