Theorem 0dif 4340

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

Syntax hints:   = wceq 1547   ∖ cdif 3887   ⊆ wss 3890  ∅c0 4268

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-dif 3893  df-ss 3907  df-nul 4269

This theorem is referenced by:  symdif0  5021  fresaun  6705  dffv2  6929  nulchn  18583  chnccat  18590  ablfac1eulem  20047  itgioo  25808  newval  27852  imadifxp  32697  sibf0  34525  ballotlemfval0  34687  ballotlemgun  34716  satf0  35607  mdvval  35739  fzdifsuc2  45765  ibliooicc  46421  disjdifb  49307