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.

Step	Hyp	Ref	Expression
1		noel 4338	. . . 4 ⊢ ¬ ⟨𝑥, 𝑦⟩ ∈ ∅
2	1	nex 1800	. . 3 ⊢ ¬ ∃𝑦⟨𝑥, 𝑦⟩ ∈ ∅
3		vex 3484	. . . 4 ⊢ 𝑥 ∈ V
4	3	eldm2 5912	. . 3 ⊢ (𝑥 ∈ dom ∅ ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ ∅)
5	2, 4	mtbir 323	. 2 ⊢ ¬ 𝑥 ∈ dom ∅
6	5	nel0 4354	1 ⊢ dom ∅ = ∅

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