Theorem dif0 4330

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

Syntax hints:   = wceq 1541   ∖ cdif 3898  ∅c0 4285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-nul 4286

This theorem is referenced by:  unvdif  4427  disjdif2  4432  csbdif  4478  iinvdif  5035  symdif0  5040  dffv2  6929  2oconcl  8430  oe0m0  8447  oev2  8450  infdiffi  9567  cnfcom2lem  9610  brttrcl2  9623  ttrcltr  9625  rnttrcl  9631  m1bits  16367  mreexdomd  17572  efgi0  19649  vrgpinv  19698  frgpuptinv  19700  frgpnabllem1  19802  gsumval3  19836  gsumcllem  19837  dprddisj2  19970  0cld  22982  indiscld  23035  mretopd  23036  hauscmplem  23350  cfinfil  23837  csdfil  23838  filufint  23864  bcth3  25287  rembl  25497  volsup  25513  new0  27860  disjdifprg  32650  indconst0  32939  tocycf  33199  tocyc01  33200  prsiga  34288  sigapildsyslem  34318  sigapildsys  34319  sxbrsigalem3  34429  0elcarsg  34464  carsgclctunlem3  34477  onint1  36643  lindsdom  37815  oe0rif  43527  tfsconcat0i  43587  ntrclscls00  44307  ntrclskb  44310  compne  44681  prsal  46562  saluni  46569  caragen0  46750  carageniuncllem1  46765  iscnrm3rlem4  49188  aacllem  50046