Theorem 0dif 4359

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

Step	Hyp	Ref	Expression
1		difss 4090	. 2 ⊢ (∅ ∖ 𝐴) ⊆ ∅
2		ss0 4356	. 2 ⊢ ((∅ ∖ 𝐴) ⊆ ∅ → (∅ ∖ 𝐴) = ∅)
3	1, 2	ax-mp 5	1 ⊢ (∅ ∖ 𝐴) = ∅

Syntax hints:   = wceq 1542   ∖ cdif 3900   ⊆ wss 3903  ∅c0 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-dif 3906  df-ss 3920  df-nul 4288

This theorem is referenced by:  symdif0  5042  fresaun  6713  dffv2  6937  nulchn  18554  chnccat  18561  ablfac1eulem  20015  itgioo  25785  newval  27843  imadifxp  32687  sibf0  34511  ballotlemfval0  34673  ballotlemgun  34702  satf0  35585  mdvval  35717  fzdifsuc2  45669  ibliooicc  46326  disjdifb  49166