Theorem dif0 4341

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

Syntax hints:   = wceq 1540   ∖ cdif 3911  ∅c0 4296

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 3406  df-v 3449  df-dif 3917  df-nul 4297

This theorem is referenced by:  unvdif  4438  disjdif2  4443  csbdif  4487  iinvdif  5044  symdif0  5049  dffv2  6956  2oconcl  8467  oe0m0  8484  oev2  8487  infdiffi  9611  cnfcom2lem  9654  brttrcl2  9667  ttrcltr  9669  rnttrcl  9675  m1bits  16410  mreexdomd  17610  efgi0  19650  vrgpinv  19699  frgpuptinv  19701  frgpnabllem1  19803  gsumval3  19837  gsumcllem  19838  dprddisj2  19971  0cld  22925  indiscld  22978  mretopd  22979  hauscmplem  23293  cfinfil  23780  csdfil  23781  filufint  23807  bcth3  25231  rembl  25441  volsup  25457  new0  27786  disjdifprg  32504  tocycf  33074  tocyc01  33075  prsiga  34121  sigapildsyslem  34151  sigapildsys  34152  sxbrsigalem3  34263  0elcarsg  34298  carsgclctunlem3  34311  onint1  36437  lindsdom  37608  oe0rif  43274  tfsconcat0i  43334  ntrclscls00  44055  ntrclskb  44058  compne  44430  prsal  46316  saluni  46323  caragen0  46504  carageniuncllem1  46519  iscnrm3rlem4  48931  aacllem  49790