Theorem dif0 4306

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 4304	. . 3 ⊢ (𝐴 ∖ 𝐴) = ∅
2	1	difeq2i 4054	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = (𝐴 ∖ ∅)
3		difdif 4065	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = 𝐴
4	2, 3	eqtr3i 2768	1 ⊢ (𝐴 ∖ ∅) = 𝐴

Syntax hints:   = wceq 1539   ∖ cdif 3884  ∅c0 4256

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-nul 4257

This theorem is referenced by:  unvdif  4408  disjdif2  4413  csbdif  4458  iinvdif  5009  symdif0  5014  dffv2  6863  2oconcl  8333  oe0m0  8350  oev2  8353  infdiffi  9416  cnfcom2lem  9459  brttrcl2  9472  ttrcltr  9474  rnttrcl  9480  m1bits  16147  mreexdomd  17358  efgi0  19326  vrgpinv  19375  frgpuptinv  19377  frgpnabllem1  19474  gsumval3  19508  gsumcllem  19509  dprddisj2  19642  0cld  22189  indiscld  22242  mretopd  22243  hauscmplem  22557  cfinfil  23044  csdfil  23045  filufint  23071  bcth3  24495  rembl  24704  volsup  24720  disjdifprg  30914  tocycf  31384  tocyc01  31385  prsiga  32099  sigapildsyslem  32129  sigapildsys  32130  sxbrsigalem3  32239  0elcarsg  32274  carsgclctunlem3  32287  new0  34058  onint1  34638  lindsdom  35771  ntrclscls00  41676  ntrclskb  41679  compne  42059  prsal  43859  saluni  43865  caragen0  44044  carageniuncllem1  44059  iscnrm3rlem4  46237  aacllem  46505