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

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

Proof of Theorem rexex
StepHypRef Expression
1 df-rex 3071 . 2 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
2 exsimpr 1873 . 2 (∃𝑥(𝑥𝐴𝜑) → ∃𝑥𝜑)
31, 2sylbi 216 1 (∃𝑥𝐴 𝜑 → ∃𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wex 1782  wcel 2107  wrex 3070
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 3071
This theorem is referenced by:  reu3  3686  rmo2i  3845  dffo5  7055  el2xpss  7970  nqerf  10871  supsrlem  11052  vdwmc2  16856  toprntopon  22290  isch3  30225  19.9d2rf  31442  volfiniune  32886  bnj594  33581  bnj1371  33698  bnj1374  33700  loop1cycl  33788  umgr2cycllem  33791  umgr2cycl  33792  dfrdg4  34582  bj-0nelsngl  35488  bj-ccinftydisj  35730  poimirlem25  36149  mblfinlem3  36163  mblfinlem4  36164  clsk3nimkb  42400  grumnudlem  42653  ismnushort  42669  stoweidlem57  44384
  Copyright terms: Public domain W3C validator