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

Theorem dm0 4880
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
StepHypRef Expression
1 eq0 3444 . 2  |-  ( dom  (/)  =  (/)  <->  A. x  -.  x  e.  dom  (/) )
2 noel 3434 . . . 4  |-  -.  <. x ,  y >.  e.  (/)
32nex 1587 . . 3  |-  -.  E. y <. x ,  y
>.  e.  (/)
4 vex 2766 . . . 4  |-  x  e. 
_V
54eldm2 4865 . . 3  |-  ( x  e.  dom  (/)  <->  E. y <. x ,  y >.  e.  (/) )
63, 5mtbir 292 . 2  |-  -.  x  e.  dom  (/)
71, 6mpgbir 1544 1  |-  dom  (/)  =  (/)
Colors of variables: wff set class
Syntax hints:   -. wn 5   E.wex 1537    = wceq 1619    e. wcel 1621   (/)c0 3430   <.cop 3617   dom cdm 4661
This theorem is referenced by:  dmxpid  4886  rn0  4924  dmxpss  5095  fn0  5301  f1o00  5446  fv01  5493  1stval  6058  tz7.44lem1  6386  tz7.44-2  6388  tz7.44-3  6389  oicl  7212  oif  7213  strlemor0  13197  dvbsss  19215  perfdvf  19216  ismgm  20948  dmadjrnb  22447  umgra0  23250  eupa0  23271  0alg  25124  0ded  25125  0catOLD  25126  symgsssg  26776  symgfisg  26777  psgnunilem5  26785
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ne 2423  df-rab 2527  df-v 2765  df-dif 3130  df-un 3132  df-in 3134  df-ss 3141  df-nul 3431  df-if 3540  df-sn 3620  df-pr 3621  df-op 3623  df-br 3998  df-dm 4679
  Copyright terms: Public domain W3C validator