Theorem dif0 4331

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

Syntax hints:   = wceq 1540   ∖ cdif 3902  ∅c0 4286

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-nul 4287

This theorem is referenced by:  unvdif  4428  disjdif2  4433  csbdif  4477  iinvdif  5032  symdif0  5037  dffv2  6922  2oconcl  8428  oe0m0  8445  oev2  8448  infdiffi  9573  cnfcom2lem  9616  brttrcl2  9629  ttrcltr  9631  rnttrcl  9637  m1bits  16369  mreexdomd  17573  efgi0  19617  vrgpinv  19666  frgpuptinv  19668  frgpnabllem1  19770  gsumval3  19804  gsumcllem  19805  dprddisj2  19938  0cld  22941  indiscld  22994  mretopd  22995  hauscmplem  23309  cfinfil  23796  csdfil  23797  filufint  23823  bcth3  25247  rembl  25457  volsup  25473  new0  27806  disjdifprg  32537  tocycf  33072  tocyc01  33073  prsiga  34100  sigapildsyslem  34130  sigapildsys  34131  sxbrsigalem3  34242  0elcarsg  34277  carsgclctunlem3  34290  onint1  36425  lindsdom  37596  oe0rif  43261  tfsconcat0i  43321  ntrclscls00  44042  ntrclskb  44045  compne  44417  prsal  46303  saluni  46310  caragen0  46491  carageniuncllem1  46506  iscnrm3rlem4  48931  aacllem  49790