Theorem dm0 5902

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 4284	. . . 4 ⊢ ¬ ⟨𝑥, 𝑦⟩ ∈ ∅
2	1	nex 1833	. . 3 ⊢ ¬ ∃𝑦⟨𝑥, 𝑦⟩ ∈ ∅
3		vex 3455	. . . 4 ⊢ 𝑥 ∈ V
4	3	eldm2 5883	. . 3 ⊢ (𝑥 ∈ dom ∅ ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ ∅)
5	2, 4	mtbir 326	. 2 ⊢ ¬ 𝑥 ∈ dom ∅
6	5	nel0 4302	1 ⊢ dom ∅ = ∅

This proof depends on syntax axioms:   = wceq 1570  ∃wex 1812   ∈ wcel 2145  ∅c0 4279  ⟨cop 4590  dom cdm 5651

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-dm 5661

This theorem is used by:  rn0  5908  dmxpid  5912  dmxpss  6162  fn0  6662  f0dom0  6758  f10d  6851  f1o00  6852  0fv  6918  1stval  7992  bropopvvv  8090  bropfvvvv  8092  supp0  8166  tz7.44lem1  8397  tz7.44-2  8399  tz7.44-3  8400  oicl  9507  oif  9508  swrd0  14788  dmtrclfv  15151  relexpdmd  15177  nulchn  18773  symgsssg  19661  symgfisg  19662  psgnunilem5  19688  matunitlindf  22976  dvbsss  26202  perfdvf  26203  uhgr0e  29631  uhgr0  29633  usgr0  29806  egrsubgr  29840  0grsubgr  29841  vtxdg0e  30037  eupth0  30797  dmadjrnb  32490  eldmne0  33203  of0r  33255  f1ocnt  33374  tocyccntz  33687  mbfmcst  34874  0rrv  35066  ismgmOLD  38752  conrel2d  44623  neicvgbex  45071  iblempty  46919  dmrnxp  49891  reldmprcof1  50433  reldmprcof2  50434  reldmlan2  50669  reldmran2  50670