Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  dm0 Structured version   Visualization version   GIF version

Theorem dm0 5788
 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.
StepHypRef Expression
1 noel 4299 . . . 4 ¬ ⟨𝑥, 𝑦⟩ ∈ ∅
21nex 1794 . . 3 ¬ ∃𝑦𝑥, 𝑦⟩ ∈ ∅
3 vex 3502 . . . 4 𝑥 ∈ V
43eldm2 5768 . . 3 (𝑥 ∈ dom ∅ ↔ ∃𝑦𝑥, 𝑦⟩ ∈ ∅)
52, 4mtbir 324 . 2 ¬ 𝑥 ∈ dom ∅
65nel0 4314 1 dom ∅ = ∅
 Colors of variables: wff setvar class Syntax hints:   = wceq 1530  ∃wex 1773   ∈ wcel 2106  ∅c0 4294  ⟨cop 4569  dom cdm 5553 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2152  ax-12 2167  ax-ext 2796 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2803  df-cleq 2817  df-clel 2897  df-nfc 2967  df-rab 3151  df-v 3501  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4470  df-sn 4564  df-pr 4566  df-op 4570  df-br 5063  df-dm 5563 This theorem is referenced by:  rn0  5794  dmxpid  5798  dmxpss  6025  fn0  6475  f0dom0  6559  f10d  6644  f1o00  6645  0fv  6705  1stval  7685  bropopvvv  7779  bropfvvvv  7781  supp0  7829  tz7.44lem1  8035  tz7.44-2  8037  tz7.44-3  8038  oicl  8985  oif  8986  swrd0  14013  dmtrclfv  14371  symgsssg  18517  symgfisg  18518  psgnunilem5  18544  dvbsss  24415  perfdvf  24416  uhgr0e  26771  uhgr0  26773  usgr0  26940  egrsubgr  26974  0grsubgr  26975  vtxdg0e  27171  eupth0  27908  dmadjrnb  29598  eldmne0  30289  f1ocnt  30439  tocyccntz  30701  mbfmcst  31404  0rrv  31596  matunitlindf  34758  ismgmOLD  34997  conrel2d  39871  neicvgbex  40324  iblempty  42112
 Copyright terms: Public domain W3C validator