Theorem dm0 5933

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 4343	. . . 4 ⊢ ¬ ⟨𝑥, 𝑦⟩ ∈ ∅
2	1	nex 1796	. . 3 ⊢ ¬ ∃𝑦⟨𝑥, 𝑦⟩ ∈ ∅
3		vex 3481	. . . 4 ⊢ 𝑥 ∈ V
4	3	eldm2 5914	. . 3 ⊢ (𝑥 ∈ dom ∅ ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ ∅)
5	2, 4	mtbir 323	. 2 ⊢ ¬ 𝑥 ∈ dom ∅
6	5	nel0 4359	1 ⊢ dom ∅ = ∅

Syntax hints:   = wceq 1536  ∃wex 1775   ∈ wcel 2105  ∅c0 4338  ⟨cop 4636  dom cdm 5688

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-dm 5698

This theorem is referenced by:  rn0  5938  dmxpid  5943  dmxpss  6192  fn0  6699  f0dom0  6792  f10d  6882  f1o00  6883  0fv  6950  1stval  8014  bropopvvv  8113  bropfvvvv  8115  supp0  8188  tz7.44lem1  8443  tz7.44-2  8445  tz7.44-3  8446  oicl  9566  oif  9567  swrd0  14692  dmtrclfv  15053  relexpdmd  15079  symgsssg  19499  symgfisg  19500  psgnunilem5  19526  dvbsss  25951  perfdvf  25952  uhgr0e  29102  uhgr0  29104  usgr0  29274  egrsubgr  29308  0grsubgr  29309  vtxdg0e  29506  eupth0  30242  dmadjrnb  31934  eldmne0  32644  of0r  32694  f1ocnt  32809  tocyccntz  33146  mbfmcst  34240  0rrv  34432  matunitlindf  37604  ismgmOLD  37836  conrel2d  43653  neicvgbex  44101  iblempty  45920