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

Theorem dm0 5931
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 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 noel 4338 . . . 4 ¬ ⟨𝑥, 𝑦⟩ ∈ ∅
21nex 1800 . . 3 ¬ ∃𝑦𝑥, 𝑦⟩ ∈ ∅
3 vex 3484 . . . 4 𝑥 ∈ V
43eldm2 5912 . . 3 (𝑥 ∈ dom ∅ ↔ ∃𝑦𝑥, 𝑦⟩ ∈ ∅)
52, 4mtbir 323 . 2 ¬ 𝑥 ∈ dom ∅
65nel0 4354 1 dom ∅ = ∅
Colors of variables: wff setvar class
Syntax hints:   = wceq 1540  wex 1779  wcel 2108  c0 4333  cop 4632  dom cdm 5685
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-dm 5695
This theorem is referenced by:  rn0  5936  dmxpid  5941  dmxpss  6191  fn0  6699  f0dom0  6792  f10d  6882  f1o00  6883  0fv  6950  1stval  8016  bropopvvv  8115  bropfvvvv  8117  supp0  8190  tz7.44lem1  8445  tz7.44-2  8447  tz7.44-3  8448  oicl  9569  oif  9570  swrd0  14696  dmtrclfv  15057  relexpdmd  15083  symgsssg  19485  symgfisg  19486  psgnunilem5  19512  dvbsss  25937  perfdvf  25938  uhgr0e  29088  uhgr0  29090  usgr0  29260  egrsubgr  29294  0grsubgr  29295  vtxdg0e  29492  eupth0  30233  dmadjrnb  31925  eldmne0  32638  of0r  32688  f1ocnt  32804  tocyccntz  33164  mbfmcst  34261  0rrv  34453  matunitlindf  37625  ismgmOLD  37857  conrel2d  43677  neicvgbex  44125  iblempty  45980
  Copyright terms: Public domain W3C validator