Theorem dm0 5864

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 4287	. . . 4 ⊢ ¬ ⟨𝑥, 𝑦⟩ ∈ ∅
2	1	nex 1801	. . 3 ⊢ ¬ ∃𝑦⟨𝑥, 𝑦⟩ ∈ ∅
3		vex 3441	. . . 4 ⊢ 𝑥 ∈ V
4	3	eldm2 5845	. . 3 ⊢ (𝑥 ∈ dom ∅ ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ ∅)
5	2, 4	mtbir 323	. 2 ⊢ ¬ 𝑥 ∈ dom ∅
6	5	nel0 4303	1 ⊢ dom ∅ = ∅

Syntax hints:   = wceq 1541  ∃wex 1780   ∈ wcel 2113  ∅c0 4282  ⟨cop 4581  dom cdm 5619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-br 5094  df-dm 5629

This theorem is referenced by:  rn0  5870  dmxpid  5874  dmxpss  6123  fn0  6617  f0dom0  6712  f10d  6802  f1o00  6803  0fv  6869  1stval  7929  bropopvvv  8026  bropfvvvv  8028  supp0  8101  tz7.44lem1  8330  tz7.44-2  8332  tz7.44-3  8333  oicl  9422  oif  9423  swrd0  14568  dmtrclfv  14927  relexpdmd  14953  nulchn  18527  symgsssg  19381  symgfisg  19382  psgnunilem5  19408  dvbsss  25831  perfdvf  25832  uhgr0e  29051  uhgr0  29053  usgr0  29223  egrsubgr  29257  0grsubgr  29258  vtxdg0e  29455  eupth0  30196  dmadjrnb  31888  eldmne0  32611  of0r  32664  f1ocnt  32787  tocyccntz  33120  mbfmcst  34293  0rrv  34485  matunitlindf  37679  ismgmOLD  37911  conrel2d  43782  neicvgbex  44230  iblempty  46088  dmrnxp  48962  reldmprcof1  49507  reldmprcof2  49508  reldmlan2  49743  reldmran2  49744