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

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

Proof of Theorem rexex
StepHypRef Expression
1 df-rex 3138 . 2 (∃𝑥𝐴 𝜑 ↔ ∃𝑥(𝑥𝐴𝜑))
2 exsimpr 1871 . 2 (∃𝑥(𝑥𝐴𝜑) → ∃𝑥𝜑)
31, 2sylbi 220 1 (∃𝑥𝐴 𝜑 → ∃𝑥𝜑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399  ∃wex 1781   ∈ wcel 2115  ∃wrex 3133 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-rex 3138 This theorem is referenced by:  reu3  3703  rmo2i  3854  dffo5  6851  nqerf  10337  supsrlem  10518  vdwmc2  16302  toprntopon  21519  isch3  29013  19.9d2rf  30230  volfiniune  31507  bnj594  32202  bnj1371  32319  bnj1374  32321  loop1cycl  32402  umgr2cycllem  32405  umgr2cycl  32406  dfrdg4  33430  bj-0nelsngl  34311  bj-ccinftydisj  34531  poimirlem25  34982  mblfinlem3  34996  mblfinlem4  34997  clsk3nimkb  40578  grumnudlem  40829  stoweidlem57  42541
 Copyright terms: Public domain W3C validator