Theorem dif0 4329

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 4327	. . 3 ⊢ (𝐴 ∖ 𝐴) = ∅
2	1	difeq2i 4074	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = (𝐴 ∖ ∅)
3		difdif 4086	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = 𝐴
4	2, 3	eqtr3i 2758	1 ⊢ (𝐴 ∖ ∅) = 𝐴

Syntax hints:   = wceq 1541   ∖ cdif 3896  ∅c0 4284

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-rab 3398  df-v 3440  df-dif 3902  df-nul 4285

This theorem is referenced by:  unvdif  4426  disjdif2  4431  csbdif  4475  iinvdif  5032  symdif0  5037  dffv2  6926  2oconcl  8427  oe0m0  8444  oev2  8447  infdiffi  9558  cnfcom2lem  9601  brttrcl2  9614  ttrcltr  9616  rnttrcl  9622  m1bits  16361  mreexdomd  17565  efgi0  19642  vrgpinv  19691  frgpuptinv  19693  frgpnabllem1  19795  gsumval3  19829  gsumcllem  19830  dprddisj2  19963  0cld  22963  indiscld  23016  mretopd  23017  hauscmplem  23331  cfinfil  23818  csdfil  23819  filufint  23845  bcth3  25268  rembl  25478  volsup  25494  new0  27829  disjdifprg  32566  tocycf  33097  tocyc01  33098  prsiga  34155  sigapildsyslem  34185  sigapildsys  34186  sxbrsigalem3  34296  0elcarsg  34331  carsgclctunlem3  34344  onint1  36504  lindsdom  37664  oe0rif  43392  tfsconcat0i  43452  ntrclscls00  44173  ntrclskb  44176  compne  44547  prsal  46430  saluni  46437  caragen0  46618  carageniuncllem1  46633  iscnrm3rlem4  49057  aacllem  49916