Theorem dm0 5912

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 4292	. . . 4 ⊢ ¬ ⟨𝑥, 𝑦⟩ ∈ ∅
2	1	nex 1830	. . 3 ⊢ ¬ ∃𝑦⟨𝑥, 𝑦⟩ ∈ ∅
3		vex 3459	. . . 4 ⊢ 𝑥 ∈ V
4	3	eldm2 5893	. . 3 ⊢ (𝑥 ∈ dom ∅ ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ ∅)
5	2, 4	mtbir 326	. 2 ⊢ ¬ 𝑥 ∈ dom ∅
6	5	nel0 4310	1 ⊢ dom ∅ = ∅

Syntax hints:   = wceq 1570  ∃wex 1809   ∈ wcel 2143  ∅c0 4287  ⟨cop 4596  dom cdm 5663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-dm 5673

This theorem is referenced by:  rn0  5918  dmxpid  5922  dmxpss  6171  fn0  6668  f0dom0  6764  f10d  6857  f1o00  6858  0fv  6924  1stval  7989  bropopvvv  8086  bropfvvvv  8088  supp0  8162  tz7.44lem1  8393  tz7.44-2  8395  tz7.44-3  8396  oicl  9492  oif  9493  swrd0  14698  dmtrclfv  15057  relexpdmd  15083  nulchn  18676  symgsssg  19538  symgfisg  19539  psgnunilem5  19565  dvbsss  26042  perfdvf  26043  uhgr0e  29399  uhgr0  29401  usgr0  29571  egrsubgr  29605  0grsubgr  29606  vtxdg0e  29802  eupth0  30543  dmadjrnb  32236  eldmne0  32950  of0r  33002  f1ocnt  33123  tocyccntz  33442  mbfmcst  34627  0rrv  34819  matunitlindf  38247  ismgmOLD  38479  conrel2d  44370  neicvgbex  44818  iblempty  46659  dmrnxp  49592  reldmprcof1  50136  reldmprcof2  50137  reldmlan2  50372  reldmran2  50373