MPE Home 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