Theorem dm0 5754

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 4247	. . . 4 ⊢ ¬ ⟨𝑥, 𝑦⟩ ∈ ∅
2	1	nex 1802	. . 3 ⊢ ¬ ∃𝑦⟨𝑥, 𝑦⟩ ∈ ∅
3		vex 3444	. . . 4 ⊢ 𝑥 ∈ V
4	3	eldm2 5734	. . 3 ⊢ (𝑥 ∈ dom ∅ ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ ∅)
5	2, 4	mtbir 326	. 2 ⊢ ¬ 𝑥 ∈ dom ∅
6	5	nel0 4264	1 ⊢ dom ∅ = ∅

Syntax hints:   = wceq 1538  ∃wex 1781   ∈ wcel 2111  ∅c0 4243  ⟨cop 4531  dom cdm 5519

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-v 3443  df-dif 3884  df-un 3886  df-nul 4244  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-dm 5529

This theorem is referenced by:  rn0  5760  dmxpid  5764  dmxpss  5995  fn0  6451  f0dom0  6537  f10d  6623  f1o00  6624  0fv  6684  1stval  7673  bropopvvv  7768  bropfvvvv  7770  supp0  7818  tz7.44lem1  8024  tz7.44-2  8026  tz7.44-3  8027  oicl  8977  oif  8978  swrd0  14011  dmtrclfv  14369  relexpdmd  14395  symgsssg  18587  symgfisg  18588  psgnunilem5  18614  dvbsss  24505  perfdvf  24506  uhgr0e  26864  uhgr0  26866  usgr0  27033  egrsubgr  27067  0grsubgr  27068  vtxdg0e  27264  eupth0  27999  dmadjrnb  29689  eldmne0  30387  f1ocnt  30551  tocyccntz  30836  mbfmcst  31627  0rrv  31819  matunitlindf  35055  ismgmOLD  35288  conrel2d  40365  neicvgbex  40815  iblempty  42607