Theorem dm0 5901

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 4293	. . . 4 ⊢ ¬ ⟨𝑥, 𝑦⟩ ∈ ∅
2	1	nex 1823	. . 3 ⊢ ¬ ∃𝑦⟨𝑥, 𝑦⟩ ∈ ∅
3		vex 3461	. . . 4 ⊢ 𝑥 ∈ V
4	3	eldm2 5882	. . 3 ⊢ (𝑥 ∈ dom ∅ ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ ∅)
5	2, 4	mtbir 326	. 2 ⊢ ¬ 𝑥 ∈ dom ∅
6	5	nel0 4310	1 ⊢ dom ∅ = ∅

Syntax hints:   = wceq 1563  ∃wex 1802   ∈ wcel 2145  ∅c0 4288  ⟨cop 4591  dom cdm 5652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5106  df-dm 5662

This theorem is referenced by:  rn0  5907  dmxpid  5911  dmxpss  6161  fn0  6656  f0dom0  6752  f10d  6845  f1o00  6846  0fv  6912  1stval  7976  bropopvvv  8073  bropfvvvv  8075  supp0  8149  tz7.44lem1  8380  tz7.44-2  8382  tz7.44-3  8383  oicl  9479  oif  9480  swrd0  14686  dmtrclfv  15045  relexpdmd  15071  nulchn  18665  symgsssg  19528  symgfisg  19529  psgnunilem5  19555  dvbsss  26022  perfdvf  26023  uhgr0e  29330  uhgr0  29332  usgr0  29502  egrsubgr  29536  0grsubgr  29537  vtxdg0e  29733  eupth0  30474  dmadjrnb  32167  eldmne0  32884  of0r  32936  f1ocnt  33057  tocyccntz  33377  mbfmcst  34566  0rrv  34758  matunitlindf  38129  ismgmOLD  38361  conrel2d  44252  neicvgbex  44700  iblempty  46537  dmrnxp  49466  reldmprcof1  50010  reldmprcof2  50011  reldmlan2  50246  reldmran2  50247