Theorem dm0 5829

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 4264	. . . 4 ⊢ ¬ ⟨𝑥, 𝑦⟩ ∈ ∅
2	1	nex 1803	. . 3 ⊢ ¬ ∃𝑦⟨𝑥, 𝑦⟩ ∈ ∅
3		vex 3436	. . . 4 ⊢ 𝑥 ∈ V
4	3	eldm2 5810	. . 3 ⊢ (𝑥 ∈ dom ∅ ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ ∅)
5	2, 4	mtbir 323	. 2 ⊢ ¬ 𝑥 ∈ dom ∅
6	5	nel0 4284	1 ⊢ dom ∅ = ∅

Syntax hints:   = wceq 1539  ∃wex 1782   ∈ wcel 2106  ∅c0 4256  ⟨cop 4567  dom cdm 5589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-dm 5599

This theorem is referenced by:  rn0  5835  dmxpid  5839  dmxpss  6074  fn0  6564  f0dom0  6658  f10d  6750  f1o00  6751  0fv  6813  1stval  7833  bropopvvv  7930  bropfvvvv  7932  supp0  7982  tz7.44lem1  8236  tz7.44-2  8238  tz7.44-3  8239  oicl  9288  oif  9289  swrd0  14371  dmtrclfv  14729  relexpdmd  14755  symgsssg  19075  symgfisg  19076  psgnunilem5  19102  dvbsss  25066  perfdvf  25067  uhgr0e  27441  uhgr0  27443  usgr0  27610  egrsubgr  27644  0grsubgr  27645  vtxdg0e  27841  eupth0  28578  dmadjrnb  30268  eldmne0  30963  f1ocnt  31123  tocyccntz  31411  mbfmcst  32226  0rrv  32418  matunitlindf  35775  ismgmOLD  36008  conrel2d  41272  neicvgbex  41722  iblempty  43506