Theorem 0dif 4364

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

Syntax hints:   = wceq 1570   ∖ cdif 3903   ⊆ wss 3906  ∅c0 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-dif 3909  df-ss 3923  df-nul 4288

This theorem is referenced by:  symdif0  5052  fresaun  6751  dffv2  6978  nulchn  18676  chnccat  18683  ablfac1eulem  20145  itgioo  25956  newval  28009  imadifxp  32927  sibf0  34705  ballotlemfval0  34867  ballotlemgun  34896  satf0  35845  mdvval  35977  fzdifsuc2  46012  ibliooicc  46668  disjdifb  49571