Theorem 0dif 4354

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

Syntax hints:   = wceq 1541   ∖ cdif 3895   ⊆ wss 3898  ∅c0 4282

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-dif 3901  df-ss 3915  df-nul 4283

This theorem is referenced by:  symdif0  5037  fresaun  6701  dffv2  6925  nulchn  18529  chnccat  18536  ablfac1eulem  19990  itgioo  25747  newval  27799  imadifxp  32585  sibf0  34370  ballotlemfval0  34532  ballotlemgun  34561  satf0  35439  mdvval  35571  fzdifsuc2  45438  ibliooicc  46096  disjdifb  48937