Theorem 0dif 4345

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

Syntax hints:   = wceq 1542   ∖ cdif 3886   ⊆ wss 3889  ∅c0 4273

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-dif 3892  df-ss 3906  df-nul 4274

This theorem is referenced by:  symdif0  5027  fresaun  6711  dffv2  6935  nulchn  18585  chnccat  18592  ablfac1eulem  20049  itgioo  25783  newval  27827  imadifxp  32671  sibf0  34478  ballotlemfval0  34640  ballotlemgun  34669  satf0  35554  mdvval  35686  fzdifsuc2  45743  ibliooicc  46399  disjdifb  49285