Theorem dif0 4378

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 4376	. . 3 ⊢ (𝐴 ∖ 𝐴) = ∅
2	1	difeq2i 4123	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = (𝐴 ∖ ∅)
3		difdif 4135	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = 𝐴
4	2, 3	eqtr3i 2767	1 ⊢ (𝐴 ∖ ∅) = 𝐴

Syntax hints:   = wceq 1540   ∖ cdif 3948  ∅c0 4333

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 2708

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 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-nul 4334

This theorem is referenced by:  unvdif  4475  disjdif2  4480  csbdif  4524  iinvdif  5080  symdif0  5085  dffv2  7004  2oconcl  8541  oe0m0  8558  oev2  8561  infdiffi  9698  cnfcom2lem  9741  brttrcl2  9754  ttrcltr  9756  rnttrcl  9762  m1bits  16477  mreexdomd  17692  efgi0  19738  vrgpinv  19787  frgpuptinv  19789  frgpnabllem1  19891  gsumval3  19925  gsumcllem  19926  dprddisj2  20059  0cld  23046  indiscld  23099  mretopd  23100  hauscmplem  23414  cfinfil  23901  csdfil  23902  filufint  23928  bcth3  25365  rembl  25575  volsup  25591  new0  27913  disjdifprg  32588  tocycf  33137  tocyc01  33138  prsiga  34132  sigapildsyslem  34162  sigapildsys  34163  sxbrsigalem3  34274  0elcarsg  34309  carsgclctunlem3  34322  onint1  36450  lindsdom  37621  oe0rif  43298  tfsconcat0i  43358  ntrclscls00  44079  ntrclskb  44082  compne  44460  prsal  46333  saluni  46340  caragen0  46521  carageniuncllem1  46536  iscnrm3rlem4  48840  aacllem  49320