Theorem dm0 5921

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

Syntax hints:   = wceq 1542  ∃wex 1782   ∈ wcel 2107  ∅c0 4323  ⟨cop 4635  dom cdm 5677

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-dm 5687

This theorem is referenced by:  rn0  5926  dmxpid  5930  dmxpss  6171  fn0  6682  f0dom0  6776  f10d  6868  f1o00  6869  0fv  6936  1stval  7977  bropopvvv  8076  bropfvvvv  8078  supp0  8151  tz7.44lem1  8405  tz7.44-2  8407  tz7.44-3  8408  oicl  9524  oif  9525  swrd0  14608  dmtrclfv  14965  relexpdmd  14991  symgsssg  19335  symgfisg  19336  psgnunilem5  19362  dvbsss  25419  perfdvf  25420  uhgr0e  28331  uhgr0  28333  usgr0  28500  egrsubgr  28534  0grsubgr  28535  vtxdg0e  28731  eupth0  29467  dmadjrnb  31159  eldmne0  31852  f1ocnt  32013  tocyccntz  32303  mbfmcst  33258  0rrv  33450  matunitlindf  36486  ismgmOLD  36718  conrel2d  42415  neicvgbex  42863  iblempty  44681