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

Theorem dm0 5495
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 4063 . . . 4 ¬ ⟨𝑥, 𝑦⟩ ∈ ∅
21nex 1880 . . 3 ¬ ∃𝑦𝑥, 𝑦⟩ ∈ ∅
3 vex 3344 . . . 4 𝑥 ∈ V
43eldm2 5478 . . 3 (𝑥 ∈ dom ∅ ↔ ∃𝑦𝑥, 𝑦⟩ ∈ ∅)
52, 4mtbir 312 . 2 ¬ 𝑥 ∈ dom ∅
65nel0 4076 1 dom ∅ = ∅
Colors of variables: wff setvar class
Syntax hints:   = wceq 1632  wex 1853  wcel 2140  c0 4059  cop 4328  dom cdm 5267
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-rab 3060  df-v 3343  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-nul 4060  df-if 4232  df-sn 4323  df-pr 4325  df-op 4329  df-br 4806  df-dm 5277
This theorem is referenced by:  dmxpid  5501  rn0  5533  dmxpss  5724  fn0  6173  f0dom0  6251  f10d  6333  f1o00  6334  0fv  6390  1stval  7337  bropopvvv  7425  bropfvvvv  7427  supp0  7470  tz7.44lem1  7672  tz7.44-2  7674  tz7.44-3  7675  oicl  8602  oif  8603  swrd0  13655  dmtrclfv  13979  strlemor0OLD  16191  symgsssg  18108  symgfisg  18109  psgnunilem5  18135  dvbsss  23886  perfdvf  23887  uhgr0e  26187  uhgr0  26189  usgr0  26356  egrsubgr  26390  0grsubgr  26391  vtxdg0e  26602  eupth0  27388  dmadjrnb  29096  f1ocnt  29890  mbfmcst  30652  0rrv  30844  matunitlindf  33739  ismgmOLD  33981  conrel2d  38477  neicvgbex  38931  iblempty  40703
  Copyright terms: Public domain W3C validator