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

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

Proof of Theorem rexex
StepHypRef Expression
1 df-rex 2806 . 2
2 exsimpr 1646 . 2
31, 2sylbi 195 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  E.wex 1587  e.wcel 1758  E.wrex 2801
This theorem is referenced by:  reu3  3259  rmo2i  3395  dffo5  5983  nqerf  9236  supsrlem  9415  vdwmc2  14198  isch3  25113  19.9d2rf  26331  volfiniune  27102  dfrdg4  28437  mblfinlem3  28890  mblfinlem4  28891  fperdvper  30477  stoweidlem57  30586  bnj594  32748  bnj1371  32863  bnj1374  32865  bj-0nelsngl  33309  bj-ccinftydisj  33387
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-rex 2806
  Copyright terms: Public domain W3C validator