Theorem dm0 5877

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 4292	. . . 4 ⊢ ¬ ⟨𝑥, 𝑦⟩ ∈ ∅
2	1	nex 1802	. . 3 ⊢ ¬ ∃𝑦⟨𝑥, 𝑦⟩ ∈ ∅
3		vex 3446	. . . 4 ⊢ 𝑥 ∈ V
4	3	eldm2 5858	. . 3 ⊢ (𝑥 ∈ dom ∅ ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ ∅)
5	2, 4	mtbir 323	. 2 ⊢ ¬ 𝑥 ∈ dom ∅
6	5	nel0 4308	1 ⊢ dom ∅ = ∅

Syntax hints:   = wceq 1542  ∃wex 1781   ∈ wcel 2114  ∅c0 4287  ⟨cop 4588  dom cdm 5632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-dm 5642

This theorem is referenced by:  rn0  5883  dmxpid  5887  dmxpss  6137  fn0  6631  f0dom0  6726  f10d  6816  f1o00  6817  0fv  6883  1stval  7945  bropopvvv  8042  bropfvvvv  8044  supp0  8117  tz7.44lem1  8346  tz7.44-2  8348  tz7.44-3  8349  oicl  9446  oif  9447  swrd0  14594  dmtrclfv  14953  relexpdmd  14979  nulchn  18554  symgsssg  19408  symgfisg  19409  psgnunilem5  19435  dvbsss  25871  perfdvf  25872  uhgr0e  29156  uhgr0  29158  usgr0  29328  egrsubgr  29362  0grsubgr  29363  vtxdg0e  29560  eupth0  30301  dmadjrnb  31993  eldmne0  32716  of0r  32768  f1ocnt  32890  tocyccntz  33237  mbfmcst  34436  0rrv  34628  matunitlindf  37863  ismgmOLD  38095  conrel2d  44014  neicvgbex  44462  iblempty  46317  dmrnxp  49190  reldmprcof1  49734  reldmprcof2  49735  reldmlan2  49970  reldmran2  49971