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

This proof depends on syntax axioms:   = wceq 1570   ∖ cdif 3899   ⊆ wss 3902  ∅c0 4282

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-dif 3905  df-ss 3919  df-nul 4283

This theorem is used by:  symdif0  5049  fresaun  6750  dffv2  6977  nulchn  18713  chnccat  18720  ablfac1eulem  20207  itgioo  26050  newval  28108  imadifxp  33082  sibf0  34853  ballotlemfval0  35015  ballotlemgun  35044  satf0  35959  mdvval  36091  fzdifsuc2  46151  ibliooicc  46807  disjdifb  49746