MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rexex Structured version   Visualization version   GIF version

Theorem rexex 3182
Description: Restricted existence implies existence. (Contributed by NM, 11-Nov-1995.)
Assertion
Ref Expression
rexex (∃𝑥𝐴 𝜑 → ∃𝑥𝜑)

Proof of Theorem rexex
StepHypRef Expression
1 df-rex 3095 . 2 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
2 exsimpr 1914 . 2 (∃𝑥(𝑥𝐴𝜑) → ∃𝑥𝜑)
31, 2sylbi 209 1 (∃𝑥𝐴 𝜑 → ∃𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386  wex 1823  wcel 2106  wrex 3090
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853
This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-rex 3095
This theorem is referenced by:  reu3  3607  rmo2i  3743  dffo5  6640  nqerf  10087  supsrlem  10268  vdwmc2  16087  toprntopon  21137  clwlkclwwlkfOLD  27392  isch3  28684  19.9d2rf  29904  volfiniune  30905  bnj594  31595  bnj1371  31710  bnj1374  31712  dfrdg4  32661  bj-0nelsngl  33545  bj-ccinftydisj  33704  poimirlem25  34054  mblfinlem3  34068  mblfinlem4  34069  clsk3nimkb  39286  stoweidlem57  41193
  Copyright terms: Public domain W3C validator