Theorem dm0 5869

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

Syntax hints:   = wceq 1541  ∃wex 1780   ∈ wcel 2113  ∅c0 4285  ⟨cop 4586  dom cdm 5624

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-dm 5634

This theorem is referenced by:  rn0  5875  dmxpid  5879  dmxpss  6129  fn0  6623  f0dom0  6718  f10d  6808  f1o00  6809  0fv  6875  1stval  7935  bropopvvv  8032  bropfvvvv  8034  supp0  8107  tz7.44lem1  8336  tz7.44-2  8338  tz7.44-3  8339  oicl  9434  oif  9435  swrd0  14582  dmtrclfv  14941  relexpdmd  14967  nulchn  18542  symgsssg  19396  symgfisg  19397  psgnunilem5  19423  dvbsss  25859  perfdvf  25860  uhgr0e  29144  uhgr0  29146  usgr0  29316  egrsubgr  29350  0grsubgr  29351  vtxdg0e  29548  eupth0  30289  dmadjrnb  31981  eldmne0  32705  of0r  32758  f1ocnt  32880  tocyccntz  33226  mbfmcst  34416  0rrv  34608  matunitlindf  37815  ismgmOLD  38047  conrel2d  43901  neicvgbex  44349  iblempty  46205  dmrnxp  49078  reldmprcof1  49622  reldmprcof2  49623  reldmlan2  49858  reldmran2  49859