Theorem dm0 5860

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

Syntax hints:   = wceq 1541  ∃wex 1780   ∈ wcel 2111  ∅c0 4283  ⟨cop 4582  dom cdm 5616

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-br 5092  df-dm 5626

This theorem is referenced by:  rn0  5866  dmxpid  5870  dmxpss  6118  fn0  6612  f0dom0  6707  f10d  6797  f1o00  6798  0fv  6863  1stval  7923  bropopvvv  8020  bropfvvvv  8022  supp0  8095  tz7.44lem1  8324  tz7.44-2  8326  tz7.44-3  8327  oicl  9415  oif  9416  swrd0  14563  dmtrclfv  14922  relexpdmd  14948  nulchn  18522  symgsssg  19377  symgfisg  19378  psgnunilem5  19404  dvbsss  25828  perfdvf  25829  uhgr0e  29047  uhgr0  29049  usgr0  29219  egrsubgr  29253  0grsubgr  29254  vtxdg0e  29451  eupth0  30189  dmadjrnb  31881  eldmne0  32604  of0r  32655  f1ocnt  32777  tocyccntz  33108  mbfmcst  34267  0rrv  34459  matunitlindf  37657  ismgmOLD  37889  conrel2d  43696  neicvgbex  44144  iblempty  46002  dmrnxp  48867  reldmprcof1  49412  reldmprcof2  49413  reldmlan2  49648  reldmran2  49649