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

Theorem 0dif 4411
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 4146 . 2 (∅ ∖ 𝐴) ⊆ ∅
2 ss0 4408 . 2 ((∅ ∖ 𝐴) ⊆ ∅ → (∅ ∖ 𝐴) = ∅)
31, 2ax-mp 5 1 (∅ ∖ 𝐴) = ∅
Colors of variables: wff setvar class
Syntax hints:   = wceq 1537  cdif 3960  wss 3963  c0 4339
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-dif 3966  df-ss 3980  df-nul 4340
This theorem is referenced by:  symdif0  5090  fresaun  6780  dffv2  7004  ablfac1eulem  20107  itgioo  25866  newval  27909  imadifxp  32621  sibf0  34316  ballotlemfval0  34477  ballotlemgun  34506  satf0  35357  mdvval  35489  fzdifsuc2  45261  ibliooicc  45927  disjdifb  48658
  Copyright terms: Public domain W3C validator