Theorem dm0 5818

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 4261	. . . 4 ⊢ ¬ ⟨𝑥, 𝑦⟩ ∈ ∅
2	1	nex 1804	. . 3 ⊢ ¬ ∃𝑦⟨𝑥, 𝑦⟩ ∈ ∅
3		vex 3426	. . . 4 ⊢ 𝑥 ∈ V
4	3	eldm2 5799	. . 3 ⊢ (𝑥 ∈ dom ∅ ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ ∅)
5	2, 4	mtbir 322	. 2 ⊢ ¬ 𝑥 ∈ dom ∅
6	5	nel0 4281	1 ⊢ dom ∅ = ∅

Syntax hints:   = wceq 1539  ∃wex 1783   ∈ wcel 2108  ∅c0 4253  ⟨cop 4564  dom cdm 5580

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-dm 5590

This theorem is referenced by:  rn0  5824  dmxpid  5828  dmxpss  6063  fn0  6548  f0dom0  6642  f10d  6733  f1o00  6734  0fv  6795  1stval  7806  bropopvvv  7901  bropfvvvv  7903  supp0  7953  tz7.44lem1  8207  tz7.44-2  8209  tz7.44-3  8210  oicl  9218  oif  9219  swrd0  14299  dmtrclfv  14657  relexpdmd  14683  symgsssg  18990  symgfisg  18991  psgnunilem5  19017  dvbsss  24971  perfdvf  24972  uhgr0e  27344  uhgr0  27346  usgr0  27513  egrsubgr  27547  0grsubgr  27548  vtxdg0e  27744  eupth0  28479  dmadjrnb  30169  eldmne0  30864  f1ocnt  31025  tocyccntz  31313  mbfmcst  32126  0rrv  32318  matunitlindf  35702  ismgmOLD  35935  conrel2d  41161  neicvgbex  41611  iblempty  43396