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

Theorem dm0 4891
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 3470 . 2  |-  (  dom  (/)  =  (/)  <->  A. x  -.  x  e.  dom  (/) )
2 noel 3460 . . . 4  |-  -.  <. x ,  y >.  e.  (/)
32nex 1542 . . 3  |-  -.  E. y <. x ,  y
>.  e.  (/)
4 vex 2792 . . . 4  |-  x  e. 
_V
54eldm2 4876 . . 3  |-  ( x  e.  dom  (/)  <->  E. y <. x ,  y >.  e.  (/) )
63, 5mtbir 290 . 2  |-  -.  x  e.  dom  (/)
71, 6mpgbir 1537 1  |-  dom  (/)  =  (/)
Colors of variables: wff set class
Syntax hints:   -. wn 3   E.wex 1528    = wceq 1623    e. wcel 1685   (/)c0 3456   <.cop 3644    dom cdm 4688
This theorem is referenced by:  dmxpid  4897  rn0  4935  dmxpss  5106  fn0  5329  f1o00  5474  fv01  5521  1stval  6086  tz7.44lem1  6414  tz7.44-2  6416  tz7.44-3  6417  oicl  7240  oif  7241  strlemor0  13230  dvbsss  19248  perfdvf  19249  ismgm  20981  dmadjrnb  22482  umgra0  23284  eupa0  23305  0alg  25167  0ded  25168  0catOLD  25169  symgsssg  26819  symgfisg  26820  psgnunilem5  26828
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 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-rab 2553  df-v 2791  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3457  df-if 3567  df-sn 3647  df-pr 3648  df-op 3650  df-br 4025  df-dm 4698
  Copyright terms: Public domain W3C validator