Theorem dif0 4303

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

Syntax hints:   = wceq 1539   ∖ cdif 3880  ∅c0 4253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-nul 4254

This theorem is referenced by:  unvdif  4405  disjdif2  4410  csbdif  4455  iinvdif  5005  symdif0  5010  dffv2  6845  2oconcl  8295  oe0m0  8312  oev2  8315  infdiffi  9346  cnfcom2lem  9389  m1bits  16075  mreexdomd  17275  efgi0  19241  vrgpinv  19290  frgpuptinv  19292  frgpnabllem1  19389  gsumval3  19423  gsumcllem  19424  dprddisj2  19557  0cld  22097  indiscld  22150  mretopd  22151  hauscmplem  22465  cfinfil  22952  csdfil  22953  filufint  22979  bcth3  24400  rembl  24609  volsup  24625  disjdifprg  30815  tocycf  31286  tocyc01  31287  prsiga  31999  sigapildsyslem  32029  sigapildsys  32030  sxbrsigalem3  32139  0elcarsg  32174  carsgclctunlem3  32187  brttrcl2  33700  ttrcltr  33702  rnttrcl  33708  new0  33985  onint1  34565  lindsdom  35698  ntrclscls00  41565  ntrclskb  41568  compne  41948  prsal  43749  saluni  43755  caragen0  43934  carageniuncllem1  43949  iscnrm3rlem4  46125  aacllem  46391