Theorem dm0 5900

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

Syntax hints:   = wceq 1540  ∃wex 1779   ∈ wcel 2108  ∅c0 4308  ⟨cop 4607  dom cdm 5654

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-dm 5664

This theorem is referenced by:  rn0  5905  dmxpid  5910  dmxpss  6160  fn0  6669  f0dom0  6762  f10d  6852  f1o00  6853  0fv  6920  1stval  7990  bropopvvv  8089  bropfvvvv  8091  supp0  8164  tz7.44lem1  8419  tz7.44-2  8421  tz7.44-3  8422  oicl  9543  oif  9544  swrd0  14676  dmtrclfv  15037  relexpdmd  15063  symgsssg  19448  symgfisg  19449  psgnunilem5  19475  dvbsss  25855  perfdvf  25856  uhgr0e  29050  uhgr0  29052  usgr0  29222  egrsubgr  29256  0grsubgr  29257  vtxdg0e  29454  eupth0  30195  dmadjrnb  31887  eldmne0  32606  of0r  32656  f1ocnt  32779  tocyccntz  33155  mbfmcst  34291  0rrv  34483  matunitlindf  37642  ismgmOLD  37874  conrel2d  43688  neicvgbex  44136  iblempty  45994  dmrnxp  48815  reldmprcof1  49291  reldmprcof2  49292  reldmlan2  49492  reldmran2  49493