Theorem rexex 3077

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

Syntax hints:   → wi 4   ∧ wa 397  ∃wex 1782   ∈ wcel 2107  ∃wrex 3071

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

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-rex 3072

This theorem is referenced by:  reu3  3724  rmo2i  3883  dffo5  7106  el2xpss  8023  nqerf  10925  supsrlem  11106  vdwmc2  16912  toprntopon  22427  isch3  30494  19.9d2rf  31711  volfiniune  33228  bnj594  33923  bnj1371  34040  bnj1374  34042  loop1cycl  34128  umgr2cycllem  34131  umgr2cycl  34132  dfrdg4  34923  bj-0nelsngl  35852  bj-ccinftydisj  36094  poimirlem25  36513  mblfinlem3  36527  mblfinlem4  36528  clsk3nimkb  42791  grumnudlem  43044  ismnushort  43060  stoweidlem57  44773