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

Theorem rexex 2754
Description: Restricted existence implies existence. (Contributed by NM, 11-Nov-1995.)
Assertion
Ref Expression
rexex

Proof of Theorem rexex
StepHypRef Expression
1 df-rex 2700 . 2
2 exsimpr 1637 . 2
31, 2sylbi 189 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 362  E.wex 1581  e.wcel 1749  E.wrex 2695
This theorem is referenced by:  reu3  3127  rmo2i  3261  dffo5  5830  nqerf  9045  supsrlem  9224  vdwmc2  13980  isch3  24323  19.9d2rf  25541  volfiniune  26355  dfrdg4  27683  mblfinlem3  28101  mblfinlem4  28102  stoweidlem57  29526  bnj594  31483  bnj1371  31598  bnj1374  31600  bj-0nelsngl  31911  bj-ccinftydisj  31980
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597
This theorem depends on definitions:  df-bi 179  df-an 364  df-ex 1582  df-rex 2700
  Copyright terms: Public domain W3C validator