Theorem dm0 5910

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

This proof depends on syntax axioms:   = wceq 1570  ∃wex 1812   ∈ wcel 2147  ∅c0 4281  ⟨cop 4838  dom cdm 5656

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-dm 5666

This theorem is used by:  rn0  5916  dmxpid  5920  dmxpss  6176  fn0  6695  f0dom0  6791  f10d  6885  f1o00  6886  0fv  6952  1stval  8030  bropopvvv  8129  bropfvvvv  8131  supp0  8213  tz7.44lem1  8444  tz7.44-2  8446  tz7.44-3  8447  oicl  9553  oif  9554  swrd0  14839  dmtrclfv  15203  relexpdmd  15229  nulchn  18825  symgsssg  19714  symgfisg  19715  psgnunilem5  19741  matunitlindf  23029  dvbsss  26255  perfdvf  26256  uhgr0e  29682  uhgr0  29684  usgr0  29857  egrsubgr  29891  0grsubgr  29892  vtxdg0e  30088  eupth0  30848  dmadjrnb  32541  eldmne0  33296  of0r  33347  f1ocnt  33465  tocyccntz  33781  mbfmcst  34974  0rrv  35166  ismgmOLD  38987  conrel2d  44867  neicvgbex  45315  iblempty  47190  dmrnxp  50163  reldmprcof1  50731  reldmprcof2  50732  reldmlan2  51015  reldmran2  51016