Theorem dm0 5945

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 4360	. . . 4 ⊢ ¬ ⟨𝑥, 𝑦⟩ ∈ ∅
2	1	nex 1798	. . 3 ⊢ ¬ ∃𝑦⟨𝑥, 𝑦⟩ ∈ ∅
3		vex 3492	. . . 4 ⊢ 𝑥 ∈ V
4	3	eldm2 5926	. . 3 ⊢ (𝑥 ∈ dom ∅ ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ ∅)
5	2, 4	mtbir 323	. 2 ⊢ ¬ 𝑥 ∈ dom ∅
6	5	nel0 4377	1 ⊢ dom ∅ = ∅

Syntax hints:   = wceq 1537  ∃wex 1777   ∈ wcel 2108  ∅c0 4352  ⟨cop 4654  dom cdm 5700

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-dm 5710

This theorem is referenced by:  rn0  5950  dmxpid  5955  dmxpss  6202  fn0  6711  f0dom0  6805  f10d  6896  f1o00  6897  0fv  6964  1stval  8032  bropopvvv  8131  bropfvvvv  8133  supp0  8206  tz7.44lem1  8461  tz7.44-2  8463  tz7.44-3  8464  oicl  9598  oif  9599  swrd0  14706  dmtrclfv  15067  relexpdmd  15093  symgsssg  19509  symgfisg  19510  psgnunilem5  19536  dvbsss  25957  perfdvf  25958  uhgr0e  29106  uhgr0  29108  usgr0  29278  egrsubgr  29312  0grsubgr  29313  vtxdg0e  29510  eupth0  30246  dmadjrnb  31938  eldmne0  32647  of0r  32696  f1ocnt  32807  tocyccntz  33137  mbfmcst  34224  0rrv  34416  matunitlindf  37578  ismgmOLD  37810  conrel2d  43626  neicvgbex  44074  iblempty  45886