Theorem dm0 5884

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

Syntax hints:   = wceq 1540  ∃wex 1779   ∈ wcel 2109  ∅c0 4296  ⟨cop 4595  dom cdm 5638

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-dm 5648

This theorem is referenced by:  rn0  5889  dmxpid  5894  dmxpss  6144  fn0  6649  f0dom0  6744  f10d  6834  f1o00  6835  0fv  6902  1stval  7970  bropopvvv  8069  bropfvvvv  8071  supp0  8144  tz7.44lem1  8373  tz7.44-2  8375  tz7.44-3  8376  oicl  9482  oif  9483  swrd0  14623  dmtrclfv  14984  relexpdmd  15010  symgsssg  19397  symgfisg  19398  psgnunilem5  19424  dvbsss  25803  perfdvf  25804  uhgr0e  28998  uhgr0  29000  usgr0  29170  egrsubgr  29204  0grsubgr  29205  vtxdg0e  29402  eupth0  30143  dmadjrnb  31835  eldmne0  32552  of0r  32602  f1ocnt  32725  tocyccntz  33101  mbfmcst  34250  0rrv  34442  matunitlindf  37612  ismgmOLD  37844  conrel2d  43653  neicvgbex  44101  iblempty  45963  dmrnxp  48825  reldmprcof1  49370  reldmprcof2  49371  reldmlan2  49606  reldmran2  49607