Theorem dm0 5887

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

Syntax hints:   = wceq 1540  ∃wex 1779   ∈ wcel 2109  ∅c0 4299  ⟨cop 4598  dom cdm 5641

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-dm 5651

This theorem is referenced by:  rn0  5892  dmxpid  5897  dmxpss  6147  fn0  6652  f0dom0  6747  f10d  6837  f1o00  6838  0fv  6905  1stval  7973  bropopvvv  8072  bropfvvvv  8074  supp0  8147  tz7.44lem1  8376  tz7.44-2  8378  tz7.44-3  8379  oicl  9489  oif  9490  swrd0  14630  dmtrclfv  14991  relexpdmd  15017  symgsssg  19404  symgfisg  19405  psgnunilem5  19431  dvbsss  25810  perfdvf  25811  uhgr0e  29005  uhgr0  29007  usgr0  29177  egrsubgr  29211  0grsubgr  29212  vtxdg0e  29409  eupth0  30150  dmadjrnb  31842  eldmne0  32559  of0r  32609  f1ocnt  32732  tocyccntz  33108  mbfmcst  34257  0rrv  34449  matunitlindf  37619  ismgmOLD  37851  conrel2d  43660  neicvgbex  44108  iblempty  45970  dmrnxp  48829  reldmprcof1  49374  reldmprcof2  49375  reldmlan2  49610  reldmran2  49611