Theorem dm0 5894

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 4290	. . . 4 ⊢ ¬ ⟨𝑥, 𝑦⟩ ∈ ∅
2	1	nex 1819	. . 3 ⊢ ¬ ∃𝑦⟨𝑥, 𝑦⟩ ∈ ∅
3		vex 3457	. . . 4 ⊢ 𝑥 ∈ V
4	3	eldm2 5875	. . 3 ⊢ (𝑥 ∈ dom ∅ ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ ∅)
5	2, 4	mtbir 325	. 2 ⊢ ¬ 𝑥 ∈ dom ∅
6	5	nel0 4306	1 ⊢ dom ∅ = ∅

Syntax hints:   = wceq 1559  ∃wex 1798   ∈ wcel 2141  ∅c0 4285  ⟨cop 4587  dom cdm 5645

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-dm 5655

This theorem is referenced by:  rn0  5900  dmxpid  5904  dmxpss  6153  fn0  6648  f0dom0  6744  f10d  6837  f1o00  6838  0fv  6904  1stval  7968  bropopvvv  8064  bropfvvvv  8066  supp0  8140  tz7.44lem1  8371  tz7.44-2  8373  tz7.44-3  8374  oicl  9474  oif  9475  swrd0  14669  dmtrclfv  15028  relexpdmd  15054  nulchn  18634  symgsssg  19490  symgfisg  19491  psgnunilem5  19517  dvbsss  25944  perfdvf  25945  uhgr0e  29218  uhgr0  29220  usgr0  29390  egrsubgr  29424  0grsubgr  29425  vtxdg0e  29621  eupth0  30362  dmadjrnb  32055  eldmne0  32779  of0r  32831  f1ocnt  32952  tocyccntz  33285  mbfmcst  34517  0rrv  34709  matunitlindf  38081  ismgmOLD  38313  conrel2d  44204  neicvgbex  44652  iblempty  46503  dmrnxp  49422  reldmprcof1  49966  reldmprcof2  49967  reldmlan2  50202  reldmran2  50203