Theorem dif0 4323

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

Syntax hints:   = wceq 1541   ∖ cdif 3898  ∅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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3405  df-v 3444  df-dif 3904  df-nul 4274

This theorem is referenced by:  unvdif  4425  disjdif2  4430  csbdif  4476  iinvdif  5031  symdif0  5036  dffv2  6923  2oconcl  8408  oe0m0  8425  oev2  8428  infdiffi  9519  cnfcom2lem  9562  brttrcl2  9575  ttrcltr  9577  rnttrcl  9583  m1bits  16246  mreexdomd  17455  efgi0  19421  vrgpinv  19470  frgpuptinv  19472  frgpnabllem1  19569  gsumval3  19602  gsumcllem  19603  dprddisj2  19736  0cld  22294  indiscld  22347  mretopd  22348  hauscmplem  22662  cfinfil  23149  csdfil  23150  filufint  23176  bcth3  24600  rembl  24809  volsup  24825  disjdifprg  31199  tocycf  31669  tocyc01  31670  prsiga  32395  sigapildsyslem  32425  sigapildsys  32426  sxbrsigalem3  32537  0elcarsg  32572  carsgclctunlem3  32585  new0  34166  onint1  34775  lindsdom  35927  ntrclscls00  42049  ntrclskb  42052  compne  42432  prsal  44247  saluni  44253  caragen0  44433  carageniuncllem1  44448  iscnrm3rlem4  46655  aacllem  46923