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

Theorem dm0 4971
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 3545 . 2  |-  ( dom  (/)  =  (/)  <->  A. x  -.  x  e.  dom  (/) )
2 noel 3535 . . . 4  |-  -.  <. x ,  y >.  e.  (/)
32nex 1555 . . 3  |-  -.  E. y <. x ,  y
>.  e.  (/)
4 vex 2867 . . . 4  |-  x  e. 
_V
54eldm2 4956 . . 3  |-  ( x  e.  dom  (/)  <->  E. y <. x ,  y >.  e.  (/) )
63, 5mtbir 290 . 2  |-  -.  x  e.  dom  (/)
71, 6mpgbir 1550 1  |-  dom  (/)  =  (/)
Colors of variables: wff set class
Syntax hints:   -. wn 3   E.wex 1541    = wceq 1642    e. wcel 1710   (/)c0 3531   <.cop 3719   dom cdm 4768
This theorem is referenced by:  dmxpid  4977  rn0  5015  dmxpss  5186  fn0  5442  f1o00  5588  fv01  5639  1stval  6208  tz7.44lem1  6502  tz7.44-2  6504  tz7.44-3  6505  oicl  7331  oif  7332  strlemor0  13325  dvbsss  19350  perfdvf  19351  ismgm  21093  dmadjrnb  22594  mbfmcst  23873  0rrv  23958  umgra0  24281  eupa0  24302  symgsssg  26731  symgfisg  26732  psgnunilem5  26740  bropopvvv  27432  uhgra0  27508  usgra0  27537
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-rab 2628  df-v 2866  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-sn 3722  df-pr 3723  df-op 3725  df-br 4103  df-dm 4778
  Copyright terms: Public domain W3C validator