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

Theorem dm0 4894
Description: The domain of the empty set is empty. Part of Theorem 3.8(v) of [Monk1] p. 36. (Contributed by NM, 4-Jul-1994.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
Assertion
Ref Expression
dm0  |-  dom  (/)  =  (/)

Proof of Theorem dm0
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eq0 3471 . 2  |-  ( dom  (/)  =  (/)  <->  A. x  -.  x  e.  dom  (/) )
2 noel 3461 . . . 4  |-  -.  <. x ,  y >.  e.  (/)
32nex 1544 . . 3  |-  -.  E. y <. x ,  y
>.  e.  (/)
4 vex 2793 . . . 4  |-  x  e. 
_V
54eldm2 4879 . . 3  |-  ( x  e.  dom  (/)  <->  E. y <. x ,  y >.  e.  (/) )
63, 5mtbir 290 . 2  |-  -.  x  e.  dom  (/)
71, 6mpgbir 1539 1  |-  dom  (/)  =  (/)
Colors of variables: wff set class
Syntax hints:   -. wn 3   E.wex 1530    = wceq 1625    e. wcel 1686   (/)c0 3457   <.cop 3645   dom cdm 4691
This theorem is referenced by:  dmxpid  4900  rn0  4938  dmxpss  5109  fn0  5365  f1o00  5510  fv01  5561  1stval  6126  tz7.44lem1  6420  tz7.44-2  6422  tz7.44-3  6423  oicl  7246  oif  7247  strlemor0  13236  dvbsss  19254  perfdvf  19255  ismgm  20989  dmadjrnb  22488  mbfmcst  23566  0rrv  23656  umgra0  23879  eupa0  23900  0alg  25767  0ded  25768  0catOLD  25769  symgsssg  27419  symgfisg  27420  psgnunilem5  27428  usgra0  28127
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-rab 2554  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-br 4026  df-dm 4701
  Copyright terms: Public domain W3C validator