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

Theorem dm0 5067
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 3759 . 2  |-  ( dom  (/)  =  (/)  <->  A. x  -.  x  e.  dom  (/) )
2 noel 3747 . . . 4  |-  -.  <. x ,  y >.  e.  (/)
32nex 1689 . . 3  |-  -.  E. y <. x ,  y
>.  e.  (/)
4 vex 3060 . . . 4  |-  x  e. 
_V
54eldm2 5052 . . 3  |-  ( x  e.  dom  (/)  <->  E. y <. x ,  y >.  e.  (/) )
63, 5mtbir 305 . 2  |-  -.  x  e.  dom  (/)
71, 6mpgbir 1684 1  |-  dom  (/)  =  (/)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    = wceq 1455   E.wex 1674    e. wcel 1898   (/)c0 3743   <.cop 3986   dom cdm 4853
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-br 4417  df-dm 4863
This theorem is referenced by:  dmxpid  5073  rn0  5105  dmxpss  5287  fn0  5717  f0dom0  5790  f10d  5869  f1o00  5870  0fv  5921  1stval  6822  bropopvvv  6901  bropfvvvv  6903  supp0  6946  tz7.44lem1  7149  tz7.44-2  7151  tz7.44-3  7152  oicl  8070  oif  8071  swrd0  12827  dmtrclfv  13131  strlemor0  15265  symgsssg  17157  symgfisg  17158  psgnunilem5  17184  dvbsss  22906  perfdvf  22907  uhgra0  25085  umgra0  25101  clwwlknprop  25549  2wlkonot3v  25652  2spthonot3v  25653  eupa0  25751  ismgmOLD  26097  dmadjrnb  27608  f1ocnt  28425  mbfmcst  29130  0rrv  29333  conrel2d  36301  iblempty  37880  uhgr0e  39211  uhgr0  39213  usgr0  39368  egrsubgr  39399  0grsubgr  39400  vtxdg0e  39584  uhg0e  39961
  Copyright terms: Public domain W3C validator