Theorem dm0 5867

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 4291	. . . 4 ⊢ ¬ ⟨𝑥, 𝑦⟩ ∈ ∅
2	1	nex 1800	. . 3 ⊢ ¬ ∃𝑦⟨𝑥, 𝑦⟩ ∈ ∅
3		vex 3442	. . . 4 ⊢ 𝑥 ∈ V
4	3	eldm2 5848	. . 3 ⊢ (𝑥 ∈ dom ∅ ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ ∅)
5	2, 4	mtbir 323	. 2 ⊢ ¬ 𝑥 ∈ dom ∅
6	5	nel0 4307	1 ⊢ dom ∅ = ∅

Syntax hints:   = wceq 1540  ∃wex 1779   ∈ wcel 2109  ∅c0 4286  ⟨cop 4585  dom cdm 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-dm 5633

This theorem is referenced by:  rn0  5872  dmxpid  5876  dmxpss  6124  fn0  6617  f0dom0  6712  f10d  6802  f1o00  6803  0fv  6868  1stval  7933  bropopvvv  8030  bropfvvvv  8032  supp0  8105  tz7.44lem1  8334  tz7.44-2  8336  tz7.44-3  8337  oicl  9440  oif  9441  swrd0  14583  dmtrclfv  14943  relexpdmd  14969  symgsssg  19364  symgfisg  19365  psgnunilem5  19391  dvbsss  25819  perfdvf  25820  uhgr0e  29034  uhgr0  29036  usgr0  29206  egrsubgr  29240  0grsubgr  29241  vtxdg0e  29438  eupth0  30176  dmadjrnb  31868  eldmne0  32585  of0r  32635  f1ocnt  32758  tocyccntz  33099  mbfmcst  34226  0rrv  34418  matunitlindf  37597  ismgmOLD  37829  conrel2d  43637  neicvgbex  44085  iblempty  45947  dmrnxp  48822  reldmprcof1  49367  reldmprcof2  49368  reldmlan2  49603  reldmran2  49604