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

Theorem dm0 5543
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 4120 . . . 4 ¬ ⟨𝑥, 𝑦⟩ ∈ ∅
21nex 1896 . . 3 ¬ ∃𝑦𝑥, 𝑦⟩ ∈ ∅
3 vex 3389 . . . 4 𝑥 ∈ V
43eldm2 5526 . . 3 (𝑥 ∈ dom ∅ ↔ ∃𝑦𝑥, 𝑦⟩ ∈ ∅)
52, 4mtbir 315 . 2 ¬ 𝑥 ∈ dom ∅
65nel0 4133 1 dom ∅ = ∅
Colors of variables: wff setvar class
Syntax hints:   = wceq 1653  wex 1875  wcel 2157  c0 4116  cop 4375  dom cdm 5313
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2378  ax-ext 2778
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2787  df-cleq 2793  df-clel 2796  df-nfc 2931  df-rab 3099  df-v 3388  df-dif 3773  df-un 3775  df-in 3777  df-ss 3784  df-nul 4117  df-if 4279  df-sn 4370  df-pr 4372  df-op 4376  df-br 4845  df-dm 5323
This theorem is referenced by:  dmxpid  5549  rn0  5582  dmxpss  5783  fn0  6223  f0dom0  6305  f10d  6390  f1o00  6391  0fv  6452  1stval  7404  bropopvvv  7493  bropfvvvv  7495  supp0  7538  tz7.44lem1  7741  tz7.44-2  7743  tz7.44-3  7744  oicl  8677  oif  8678  swrd0  13686  dmtrclfv  14099  symgsssg  18198  symgfisg  18199  psgnunilem5  18225  psgnunilem5OLD  18226  dvbsss  24006  perfdvf  24007  uhgr0e  26305  uhgr0  26307  usgr0  26476  egrsubgr  26510  0grsubgr  26511  vtxdg0e  26723  eupth0  27557  dmadjrnb  29289  f1ocnt  30076  mbfmcst  30836  0rrv  31029  matunitlindf  33895  ismgmOLD  34135  conrel2d  38734  neicvgbex  39187  iblempty  40919
  Copyright terms: Public domain W3C validator