Theorem dif0 4373

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 4371	. . 3 ⊢ (𝐴 ∖ 𝐴) = ∅
2	1	difeq2i 4120	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = (𝐴 ∖ ∅)
3		difdif 4131	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = 𝐴
4	2, 3	eqtr3i 2763	1 ⊢ (𝐴 ∖ ∅) = 𝐴

Syntax hints:   = wceq 1542   ∖ cdif 3946  ∅c0 4323

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-nul 4324

This theorem is referenced by:  unvdif  4475  disjdif2  4480  csbdif  4528  iinvdif  5084  symdif0  5089  dffv2  6987  2oconcl  8503  oe0m0  8520  oev2  8523  infdiffi  9653  cnfcom2lem  9696  brttrcl2  9709  ttrcltr  9711  rnttrcl  9717  m1bits  16381  mreexdomd  17593  efgi0  19588  vrgpinv  19637  frgpuptinv  19639  frgpnabllem1  19741  gsumval3  19775  gsumcllem  19776  dprddisj2  19909  0cld  22542  indiscld  22595  mretopd  22596  hauscmplem  22910  cfinfil  23397  csdfil  23398  filufint  23424  bcth3  24848  rembl  25057  volsup  25073  new0  27369  disjdifprg  31806  tocycf  32276  tocyc01  32277  prsiga  33129  sigapildsyslem  33159  sigapildsys  33160  sxbrsigalem3  33271  0elcarsg  33306  carsgclctunlem3  33319  onint1  35334  lindsdom  36482  oe0rif  42035  tfsconcat0i  42095  ntrclscls00  42817  ntrclskb  42820  compne  43200  prsal  45034  saluni  45041  caragen0  45222  carageniuncllem1  45237  iscnrm3rlem4  47576  aacllem  47848