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

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

Proof of Theorem rexex
StepHypRef Expression
1 df-rex 3068 . 2 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
2 exsimpr 1864 . 2 (∃𝑥(𝑥𝐴𝜑) → ∃𝑥𝜑)
31, 2sylbi 216 1 (∃𝑥𝐴 𝜑 → ∃𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  wex 1773  wcel 2098  wrex 3067
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-rex 3068
This theorem is referenced by:  reu3  3724  rmo2i  3883  dffo5  7119  el2xpss  8047  nqerf  10961  supsrlem  11142  vdwmc2  16955  toprntopon  22847  isch3  31071  19.9d2rf  32290  volfiniune  33882  bnj594  34576  bnj1371  34693  bnj1374  34695  loop1cycl  34780  umgr2cycllem  34783  umgr2cycl  34784  dfrdg4  35580  bj-0nelsngl  36483  bj-ccinftydisj  36725  poimirlem25  37151  mblfinlem3  37165  mblfinlem4  37166  clsk3nimkb  43501  grumnudlem  43753  ismnushort  43769  stoweidlem57  45474
  Copyright terms: Public domain W3C validator