Theorem dm0 5875

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 4278	. . . 4 ⊢ ¬ ⟨𝑥, 𝑦⟩ ∈ ∅
2	1	nex 1802	. . 3 ⊢ ¬ ∃𝑦⟨𝑥, 𝑦⟩ ∈ ∅
3		vex 3433	. . . 4 ⊢ 𝑥 ∈ V
4	3	eldm2 5856	. . 3 ⊢ (𝑥 ∈ dom ∅ ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ ∅)
5	2, 4	mtbir 323	. 2 ⊢ ¬ 𝑥 ∈ dom ∅
6	5	nel0 4294	1 ⊢ dom ∅ = ∅

Syntax hints:   = wceq 1542  ∃wex 1781   ∈ wcel 2114  ∅c0 4273  ⟨cop 4573  dom cdm 5631

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-dm 5641

This theorem is referenced by:  rn0  5881  dmxpid  5885  dmxpss  6135  fn0  6629  f0dom0  6724  f10d  6814  f1o00  6815  0fv  6881  1stval  7944  bropopvvv  8040  bropfvvvv  8042  supp0  8115  tz7.44lem1  8344  tz7.44-2  8346  tz7.44-3  8347  oicl  9444  oif  9445  swrd0  14621  dmtrclfv  14980  relexpdmd  15006  nulchn  18585  symgsssg  19442  symgfisg  19443  psgnunilem5  19469  dvbsss  25869  perfdvf  25870  uhgr0e  29140  uhgr0  29142  usgr0  29312  egrsubgr  29346  0grsubgr  29347  vtxdg0e  29543  eupth0  30284  dmadjrnb  31977  eldmne0  32700  of0r  32752  f1ocnt  32873  tocyccntz  33205  mbfmcst  34403  0rrv  34595  matunitlindf  37939  ismgmOLD  38171  conrel2d  44091  neicvgbex  44539  iblempty  46393  dmrnxp  49312  reldmprcof1  49856  reldmprcof2  49857  reldmlan2  50092  reldmran2  50093