Theorem dm0 5869

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 4273	. . . 4 ⊢ ¬ ⟨𝑥, 𝑦⟩ ∈ ∅
2	1	nex 1807	. . 3 ⊢ ¬ ∃𝑦⟨𝑥, 𝑦⟩ ∈ ∅
3		vex 3436	. . . 4 ⊢ 𝑥 ∈ V
4	3	eldm2 5850	. . 3 ⊢ (𝑥 ∈ dom ∅ ↔ ∃𝑦⟨𝑥, 𝑦⟩ ∈ ∅)
5	2, 4	mtbir 324	. 2 ⊢ ¬ 𝑥 ∈ dom ∅
6	5	nel0 4289	1 ⊢ dom ∅ = ∅

Syntax hints:   = wceq 1547  ∃wex 1786   ∈ wcel 2119  ∅c0 4268  ⟨cop 4568  dom cdm 5625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080  df-dm 5635

This theorem is referenced by:  rn0  5875  dmxpid  5879  dmxpss  6129  fn0  6623  f0dom0  6718  f10d  6808  f1o00  6809  0fv  6875  1stval  7940  bropopvvv  8036  bropfvvvv  8038  supp0  8112  tz7.44lem1  8341  tz7.44-2  8343  tz7.44-3  8344  oicl  9441  oif  9442  swrd0  14619  dmtrclfv  14978  relexpdmd  15004  nulchn  18583  symgsssg  19440  symgfisg  19441  psgnunilem5  19467  dvbsss  25894  perfdvf  25895  uhgr0e  29165  uhgr0  29167  usgr0  29337  egrsubgr  29371  0grsubgr  29372  vtxdg0e  29568  eupth0  30309  dmadjrnb  32002  eldmne0  32726  of0r  32778  f1ocnt  32899  tocyccntz  33232  mbfmcst  34450  0rrv  34642  matunitlindf  37992  ismgmOLD  38224  conrel2d  44115  neicvgbex  44563  iblempty  46415  dmrnxp  49334  reldmprcof1  49878  reldmprcof2  49879  reldmlan2  50114  reldmran2  50115