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

Theorem 0dif 4290
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 4022 . 2 (∅ ∖ 𝐴) ⊆ ∅
2 ss0 4287 . 2 ((∅ ∖ 𝐴) ⊆ ∅ → (∅ ∖ 𝐴) = ∅)
31, 2ax-mp 5 1 (∅ ∖ 𝐴) = ∅
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  cdif 3840  wss 3843  c0 4211
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3400  df-dif 3846  df-in 3850  df-ss 3860  df-nul 4212
This theorem is referenced by:  symdif0  4970  fresaun  6549  dffv2  6763  ablfac1eulem  19313  itgioo  24568  nbgr0vtx  27298  imadifxp  30514  sibf0  31871  ballotlemfval0  32032  ballotlemgun  32061  satf0  32905  mdvval  33037  fzdifsuc2  42387  ibliooicc  43054  disjdifb  45687
  Copyright terms: Public domain W3C validator