Theorem dif0 4319

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 4317	. . 3 ⊢ (𝐴 ∖ 𝐴) = ∅
2	1	difeq2i 4064	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = (𝐴 ∖ ∅)
3		difdif 4076	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = 𝐴
4	2, 3	eqtr3i 2762	1 ⊢ (𝐴 ∖ ∅) = 𝐴

Syntax hints:   = wceq 1542   ∖ cdif 3887  ∅c0 4274

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-nul 4275

This theorem is referenced by:  unvdif  4416  disjdif2  4421  csbdif  4466  iinvdif  5023  symdif0  5028  dffv2  6929  2oconcl  8431  oe0m0  8448  oev2  8451  infdiffi  9570  cnfcom2lem  9613  brttrcl2  9626  ttrcltr  9628  rnttrcl  9634  indconst0  12162  m1bits  16400  mreexdomd  17606  efgi0  19686  vrgpinv  19735  frgpuptinv  19737  frgpnabllem1  19839  gsumval3  19873  gsumcllem  19874  dprddisj2  20007  0cld  23013  indiscld  23066  mretopd  23067  hauscmplem  23381  cfinfil  23868  csdfil  23869  filufint  23895  bcth3  25308  rembl  25517  volsup  25533  new0  27870  disjdifprg  32660  tocycf  33193  tocyc01  33194  prsiga  34291  sigapildsyslem  34321  sigapildsys  34322  sxbrsigalem3  34432  0elcarsg  34467  carsgclctunlem3  34480  onint1  36647  lindsdom  37949  oe0rif  43731  tfsconcat0i  43791  ntrclscls00  44511  ntrclskb  44514  compne  44885  prsal  46764  saluni  46771  caragen0  46952  carageniuncllem1  46967  iscnrm3rlem4  49430  aacllem  50288