Theorem dif0 4371

Description: The difference between a class and the empty set. Part of Exercise 4.4 of [Stoll] p. 16. (Contributed by NM, 17-Aug-2004.)

Assertion

Ref	Expression
dif0	⊢ (𝐴 ∖ ∅) = 𝐴

Proof of Theorem dif0

Step	Hyp	Ref	Expression
1		difid 4369	. . 3 ⊢ (𝐴 ∖ 𝐴) = ∅
2	1	difeq2i 4118	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = (𝐴 ∖ ∅)
3		difdif 4129	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = 𝐴
4	2, 3	eqtr3i 2762	1 ⊢ (𝐴 ∖ ∅) = 𝐴

Syntax hints:   = wceq 1541   ∖ cdif 3944  ∅c0 4321

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3950  df-nul 4322

This theorem is referenced by:  unvdif  4473  disjdif2  4478  csbdif  4526  iinvdif  5082  symdif0  5087  dffv2  6983  2oconcl  8499  oe0m0  8516  oev2  8519  infdiffi  9649  cnfcom2lem  9692  brttrcl2  9705  ttrcltr  9707  rnttrcl  9713  m1bits  16377  mreexdomd  17589  efgi0  19582  vrgpinv  19631  frgpuptinv  19633  frgpnabllem1  19735  gsumval3  19769  gsumcllem  19770  dprddisj2  19903  0cld  22533  indiscld  22586  mretopd  22587  hauscmplem  22901  cfinfil  23388  csdfil  23389  filufint  23415  bcth3  24839  rembl  25048  volsup  25064  new0  27358  disjdifprg  31793  tocycf  32263  tocyc01  32264  prsiga  33117  sigapildsyslem  33147  sigapildsys  33148  sxbrsigalem3  33259  0elcarsg  33294  carsgclctunlem3  33307  onint1  35322  lindsdom  36470  oe0rif  42020  tfsconcat0i  42080  ntrclscls00  42802  ntrclskb  42805  compne  43185  prsal  45020  saluni  45027  caragen0  45208  carageniuncllem1  45223  iscnrm3rlem4  47529  aacllem  47801