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

Theorem rel0 4810
Description: The empty set is a relation. (Contributed by NM, 26-Apr-1998.)
Assertion
Ref Expression
rel0  |-  Rel  (/)

Proof of Theorem rel0
StepHypRef Expression
1 0ss 3483 . 2  |-  (/)  C_  ( _V  X.  _V )
2 df-rel 4696 . 2  |-  ( Rel  (/) 
<->  (/)  C_  ( _V  X.  _V ) )
31, 2mpbir 200 1  |-  Rel  (/)
Colors of variables: wff set class
Syntax hints:   _Vcvv 2788    C_ wss 3152   (/)c0 3455    X. cxp 4687   Rel wrel 4694
This theorem is referenced by:  reldm0  4896  cnv0  5084  cnveq0  5130  co02  5186  co01  5187  tpos0  6264  0we1  6505  0er  6695  canthwe  8273  empos  25242  dibvalrel  31353  dicvalrelN  31375  dihvalrel  31469
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-dif 3155  df-in 3159  df-ss 3166  df-nul 3456  df-rel 4696
  Copyright terms: Public domain W3C validator