Theorem dm0 5495

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 4063	. . . 4 ⊢ ¬ ⟨𝑥, 𝑦⟩ ∈ ∅
2	1	nex 1880	. . 3 ⊢ ¬ ∃𝑦⟨𝑥, 𝑦⟩ ∈ ∅
3		vex 3344	. . . 4 ⊢ 𝑥 ∈ V
4	3	eldm2 5478	. . 3 ⊢ (𝑥 ∈ dom ∅ ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ ∅)
5	2, 4	mtbir 312	. 2 ⊢ ¬ 𝑥 ∈ dom ∅
6	5	nel0 4076	1 ⊢ dom ∅ = ∅

Syntax hints:   = wceq 1632  ∃wex 1853   ∈ wcel 2140  ∅c0 4059  ⟨cop 4328  dom cdm 5267

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-rab 3060  df-v 3343  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-nul 4060  df-if 4232  df-sn 4323  df-pr 4325  df-op 4329  df-br 4806  df-dm 5277

This theorem is referenced by:  dmxpid  5501  rn0  5533  dmxpss  5724  fn0  6173  f0dom0  6251  f10d  6333  f1o00  6334  0fv  6390  1stval  7337  bropopvvv  7425  bropfvvvv  7427  supp0  7470  tz7.44lem1  7672  tz7.44-2  7674  tz7.44-3  7675  oicl  8602  oif  8603  swrd0  13655  dmtrclfv  13979  strlemor0OLD  16191  symgsssg  18108  symgfisg  18109  psgnunilem5  18135  dvbsss  23886  perfdvf  23887  uhgr0e  26187  uhgr0  26189  usgr0  26356  egrsubgr  26390  0grsubgr  26391  vtxdg0e  26602  eupth0  27388  dmadjrnb  29096  f1ocnt  29890  mbfmcst  30652  0rrv  30844  matunitlindf  33739  ismgmOLD  33981  conrel2d  38477  neicvgbex  38931  iblempty  40703