Theorem dif0 4353

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 4351	. . 3 ⊢ (𝐴 ∖ 𝐴) = ∅
2	1	difeq2i 4098	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = (𝐴 ∖ ∅)
3		difdif 4110	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = 𝐴
4	2, 3	eqtr3i 2760	1 ⊢ (𝐴 ∖ ∅) = 𝐴

Syntax hints:   = wceq 1540   ∖ cdif 3923  ∅c0 4308

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-nul 4309

This theorem is referenced by:  unvdif  4450  disjdif2  4455  csbdif  4499  iinvdif  5056  symdif0  5061  dffv2  6974  2oconcl  8515  oe0m0  8532  oev2  8535  infdiffi  9672  cnfcom2lem  9715  brttrcl2  9728  ttrcltr  9730  rnttrcl  9736  m1bits  16459  mreexdomd  17661  efgi0  19701  vrgpinv  19750  frgpuptinv  19752  frgpnabllem1  19854  gsumval3  19888  gsumcllem  19889  dprddisj2  20022  0cld  22976  indiscld  23029  mretopd  23030  hauscmplem  23344  cfinfil  23831  csdfil  23832  filufint  23858  bcth3  25283  rembl  25493  volsup  25509  new0  27838  disjdifprg  32556  tocycf  33128  tocyc01  33129  prsiga  34162  sigapildsyslem  34192  sigapildsys  34193  sxbrsigalem3  34304  0elcarsg  34339  carsgclctunlem3  34352  onint1  36467  lindsdom  37638  oe0rif  43309  tfsconcat0i  43369  ntrclscls00  44090  ntrclskb  44093  compne  44465  prsal  46347  saluni  46354  caragen0  46535  carageniuncllem1  46550  iscnrm3rlem4  48917  aacllem  49665