Theorem dm0 5543

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 4120	. . . 4 ⊢ ¬ ⟨𝑥, 𝑦⟩ ∈ ∅
2	1	nex 1896	. . 3 ⊢ ¬ ∃𝑦⟨𝑥, 𝑦⟩ ∈ ∅
3		vex 3389	. . . 4 ⊢ 𝑥 ∈ V
4	3	eldm2 5526	. . 3 ⊢ (𝑥 ∈ dom ∅ ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ ∅)
5	2, 4	mtbir 315	. 2 ⊢ ¬ 𝑥 ∈ dom ∅
6	5	nel0 4133	1 ⊢ dom ∅ = ∅

Syntax hints:   = wceq 1653  ∃wex 1875   ∈ wcel 2157  ∅c0 4116  ⟨cop 4375  dom cdm 5313

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2378  ax-ext 2778

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2787  df-cleq 2793  df-clel 2796  df-nfc 2931  df-rab 3099  df-v 3388  df-dif 3773  df-un 3775  df-in 3777  df-ss 3784  df-nul 4117  df-if 4279  df-sn 4370  df-pr 4372  df-op 4376  df-br 4845  df-dm 5323

This theorem is referenced by:  dmxpid  5549  rn0  5582  dmxpss  5783  fn0  6223  f0dom0  6305  f10d  6390  f1o00  6391  0fv  6452  1stval  7404  bropopvvv  7493  bropfvvvv  7495  supp0  7538  tz7.44lem1  7741  tz7.44-2  7743  tz7.44-3  7744  oicl  8677  oif  8678  swrd0  13686  dmtrclfv  14099  symgsssg  18198  symgfisg  18199  psgnunilem5  18225  psgnunilem5OLD  18226  dvbsss  24006  perfdvf  24007  uhgr0e  26305  uhgr0  26307  usgr0  26476  egrsubgr  26510  0grsubgr  26511  vtxdg0e  26723  eupth0  27557  dmadjrnb  29289  f1ocnt  30076  mbfmcst  30836  0rrv  31029  matunitlindf  33895  ismgmOLD  34135  conrel2d  38734  neicvgbex  39187  iblempty  40919