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

Theorem 0dif 4362
Description: The difference between the empty set and a class. Part of Exercise 4.4 of [Stoll] p. 16. (Contributed by NM, 17-Aug-2004.)
Assertion
Ref Expression
0dif (∅ ∖ 𝐴) = ∅

Proof of Theorem 0dif
StepHypRef Expression
1 difss 4092 . 2 (∅ ∖ 𝐴) ⊆ ∅
2 ss0 4359 . 2 ((∅ ∖ 𝐴) ⊆ ∅ → (∅ ∖ 𝐴) = ∅)
31, 2ax-mp 5 1 (∅ ∖ 𝐴) = ∅
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  cdif 3908  wss 3911  c0 4283
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3446  df-dif 3914  df-in 3918  df-ss 3928  df-nul 4284
This theorem is referenced by:  symdif0  5046  fresaun  6714  dffv2  6937  ablfac1eulem  19856  itgioo  25196  newval  27207  nbgr0vtx  28346  imadifxp  31565  sibf0  32991  ballotlemfval0  33152  ballotlemgun  33181  satf0  34023  mdvval  34155  fzdifsuc2  43631  ibliooicc  44298  disjdifb  46980
  Copyright terms: Public domain W3C validator