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

Theorem 0dif 4405
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 4136 . 2 (∅ ∖ 𝐴) ⊆ ∅
2 ss0 4402 . 2 ((∅ ∖ 𝐴) ⊆ ∅ → (∅ ∖ 𝐴) = ∅)
31, 2ax-mp 5 1 (∅ ∖ 𝐴) = ∅
Colors of variables: wff setvar class
Syntax hints:   = wceq 1540  cdif 3948  wss 3951  c0 4333
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-dif 3954  df-ss 3968  df-nul 4334
This theorem is referenced by:  symdif0  5085  fresaun  6779  dffv2  7004  ablfac1eulem  20092  itgioo  25851  newval  27894  imadifxp  32614  sibf0  34336  ballotlemfval0  34498  ballotlemgun  34527  satf0  35377  mdvval  35509  fzdifsuc2  45322  ibliooicc  45986  disjdifb  48729
  Copyright terms: Public domain W3C validator