Theorem dm0 5918

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 4329	. . . 4 ⊢ ¬ ⟨𝑥, 𝑦⟩ ∈ ∅
2	1	nex 1802	. . 3 ⊢ ¬ ∃𝑦⟨𝑥, 𝑦⟩ ∈ ∅
3		vex 3478	. . . 4 ⊢ 𝑥 ∈ V
4	3	eldm2 5899	. . 3 ⊢ (𝑥 ∈ dom ∅ ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ ∅)
5	2, 4	mtbir 322	. 2 ⊢ ¬ 𝑥 ∈ dom ∅
6	5	nel0 4349	1 ⊢ dom ∅ = ∅

Syntax hints:   = wceq 1541  ∃wex 1781   ∈ wcel 2106  ∅c0 4321  ⟨cop 4633  dom cdm 5675

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-dm 5685

This theorem is referenced by:  rn0  5923  dmxpid  5927  dmxpss  6167  fn0  6678  f0dom0  6772  f10d  6864  f1o00  6865  0fv  6932  1stval  7973  bropopvvv  8072  bropfvvvv  8074  supp0  8147  tz7.44lem1  8401  tz7.44-2  8403  tz7.44-3  8404  oicl  9520  oif  9521  swrd0  14604  dmtrclfv  14961  relexpdmd  14987  symgsssg  19329  symgfisg  19330  psgnunilem5  19356  dvbsss  25410  perfdvf  25411  uhgr0e  28320  uhgr0  28322  usgr0  28489  egrsubgr  28523  0grsubgr  28524  vtxdg0e  28720  eupth0  29456  dmadjrnb  31146  eldmne0  31839  f1ocnt  32000  tocyccntz  32290  mbfmcst  33246  0rrv  33438  matunitlindf  36474  ismgmOLD  36706  conrel2d  42400  neicvgbex  42848  iblempty  44667