Theorem 0dif 4346

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 4077	. 2 ⊢ (∅ ∖ 𝐴) ⊆ ∅
2		ss0 4343	. 2 ⊢ ((∅ ∖ 𝐴) ⊆ ∅ → (∅ ∖ 𝐴) = ∅)
3	1, 2	ax-mp 5	1 ⊢ (∅ ∖ 𝐴) = ∅

Syntax hints:   = wceq 1542   ∖ cdif 3887   ⊆ wss 3890  ∅c0 4274

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 3432  df-dif 3893  df-ss 3907  df-nul 4275

This theorem is referenced by:  symdif0  5028  fresaun  6705  dffv2  6929  nulchn  18576  chnccat  18583  ablfac1eulem  20040  itgioo  25793  newval  27841  imadifxp  32686  sibf0  34494  ballotlemfval0  34656  ballotlemgun  34685  satf0  35570  mdvval  35702  fzdifsuc2  45761  ibliooicc  46417  disjdifb  49297