Theorem dm0 5765

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

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

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-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-dif 3863  df-un 3865  df-nul 4228  df-sn 4526  df-pr 4528  df-op 4532  df-br 5036  df-dm 5537

This theorem is referenced by:  rn0  5771  dmxpid  5775  dmxpss  6004  fn0  6466  f0dom0  6552  f10d  6639  f1o00  6640  0fv  6701  1stval  7700  bropopvvv  7795  bropfvvvv  7797  supp0  7845  tz7.44lem1  8056  tz7.44-2  8058  tz7.44-3  8059  oicl  9031  oif  9032  swrd0  14072  dmtrclfv  14430  relexpdmd  14456  symgsssg  18667  symgfisg  18668  psgnunilem5  18694  dvbsss  24606  perfdvf  24607  uhgr0e  26968  uhgr0  26970  usgr0  27137  egrsubgr  27171  0grsubgr  27172  vtxdg0e  27368  eupth0  28103  dmadjrnb  29793  eldmne0  30490  f1ocnt  30651  tocyccntz  30941  mbfmcst  31749  0rrv  31941  matunitlindf  35361  ismgmOLD  35594  conrel2d  40766  neicvgbex  41216  iblempty  43001