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

This proof depends on syntax axioms:   = wceq 1569  ∃wex 1811   ∈ wcel 2144  ∅c0 4278  ⟨cop 4834  dom cdm 5650

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-dm 5660

This theorem is used by:  rn0  5907  dmxpid  5911  dmxpss  6162  fn0  6670  f0dom0  6766  f10d  6859  f1o00  6860  0fv  6926  1stval  8003  bropopvvv  8101  bropfvvvv  8103  supp0  8185  tz7.44lem1  8416  tz7.44-2  8418  tz7.44-3  8419  oicl  9526  oif  9527  swrd0  14812  dmtrclfv  15176  relexpdmd  15202  nulchn  18798  symgsssg  19686  symgfisg  19687  psgnunilem5  19713  matunitlindf  23001  dvbsss  26227  perfdvf  26228  uhgr0e  29654  uhgr0  29656  usgr0  29829  egrsubgr  29863  0grsubgr  29864  vtxdg0e  30060  eupth0  30820  dmadjrnb  32513  eldmne0  33268  of0r  33320  f1ocnt  33438  tocyccntz  33751  mbfmcst  34937  0rrv  35129  ismgmOLD  38877  conrel2d  44757  neicvgbex  45205  iblempty  47068  dmrnxp  50041  reldmprcof1  50609  reldmprcof2  50610  reldmlan2  50893  reldmran2  50894