Theorem dif0 4318

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 4316	. . 3 ⊢ (𝐴 ∖ 𝐴) = ∅
2	1	difeq2i 4063	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = (𝐴 ∖ ∅)
3		difdif 4075	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = 𝐴
4	2, 3	eqtr3i 2761	1 ⊢ (𝐴 ∖ ∅) = 𝐴

Syntax hints:   = wceq 1542   ∖ cdif 3886  ∅c0 4273

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-nul 4274

This theorem is referenced by:  unvdif  4415  disjdif2  4420  csbdif  4465  iinvdif  5022  symdif0  5027  dffv2  6935  2oconcl  8438  oe0m0  8455  oev2  8458  infdiffi  9579  cnfcom2lem  9622  brttrcl2  9635  ttrcltr  9637  rnttrcl  9643  indconst0  12171  m1bits  16409  mreexdomd  17615  efgi0  19695  vrgpinv  19744  frgpuptinv  19746  frgpnabllem1  19848  gsumval3  19882  gsumcllem  19883  dprddisj2  20016  0cld  23003  indiscld  23056  mretopd  23057  hauscmplem  23371  cfinfil  23858  csdfil  23859  filufint  23885  bcth3  25298  rembl  25507  volsup  25523  new0  27856  disjdifprg  32645  tocycf  33178  tocyc01  33179  prsiga  34275  sigapildsyslem  34305  sigapildsys  34306  sxbrsigalem3  34416  0elcarsg  34451  carsgclctunlem3  34464  onint1  36631  lindsdom  37935  oe0rif  43713  tfsconcat0i  43773  ntrclscls00  44493  ntrclskb  44496  compne  44867  prsal  46746  saluni  46753  caragen0  46934  carageniuncllem1  46949  iscnrm3rlem4  49418  aacllem  50276