Theorem dm0 5908

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 1833	. . 3 ⊢ ¬ ∃𝑦⟨𝑥, 𝑦⟩ ∈ ∅
3		vex 3457	. . . 4 ⊢ 𝑥 ∈ V
4	3	eldm2 5889	. . 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 2145  ∅c0 4282  ⟨cop 4593  dom cdm 5659

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

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 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-dm 5669

This theorem is used by:  rn0  5914  dmxpid  5918  dmxpss  6168  fn0  6667  f0dom0  6763  f10d  6856  f1o00  6857  0fv  6923  1stval  7992  bropopvvv  8091  bropfvvvv  8093  supp0  8167  tz7.44lem1  8398  tz7.44-2  8400  tz7.44-3  8401  oicl  9505  oif  9506  swrd0  14732  dmtrclfv  15095  relexpdmd  15121  nulchn  18713  symgsssg  19600  symgfisg  19601  psgnunilem5  19627  matunitlindf  22909  dvbsss  26136  perfdvf  26137  uhgr0e  29536  uhgr0  29538  usgr0  29711  egrsubgr  29745  0grsubgr  29746  vtxdg0e  29942  eupth0  30702  dmadjrnb  32395  eldmne0  33108  of0r  33160  f1ocnt  33279  tocyccntz  33592  mbfmcst  34778  0rrv  34970  ismgmOLD  38608  conrel2d  44512  neicvgbex  44960  iblempty  46801  dmrnxp  49773  reldmprcof1  50315  reldmprcof2  50316  reldmlan2  50551  reldmran2  50552