Theorem dif0 4328

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

Syntax hints:   = wceq 1559   ∖ cdif 3899  ∅c0 4283

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3905  df-nul 4284

This theorem is referenced by:  unvdif  4426  disjdif2  4431  csbdif  4476  iinvdif  5034  symdif0  5039  dffv2  6956  2oconcl  8465  oe0m0  8482  oev2  8485  infdiffi  9606  cnfcom2lem  9649  brttrcl2  9662  ttrcltr  9664  rnttrcl  9670  indconst0  12200  m1bits  16464  mreexdomd  17671  efgi0  19750  vrgpinv  19799  frgpuptinv  19801  frgpnabllem1  19903  gsumval3  19937  gsumcllem  19938  dprddisj2  20071  0cld  23085  indiscld  23138  mretopd  23139  hauscmplem  23453  cfinfil  23940  csdfil  23941  filufint  23967  bcth3  25380  rembl  25589  volsup  25605  new0  27944  disjdifprg  32734  tocycf  33257  tocyc01  33258  prsiga  34388  sigapildsyslem  34418  sigapildsys  34419  sxbrsigalem3  34529  0elcarsg  34564  carsgclctunlem3  34577  onint1  36769  lindsdom  38073  oe0rif  43822  tfsconcat0i  43882  ntrclscls00  44602  ntrclskb  44605  compne  44976  prsal  46852  saluni  46859  caragen0  47040  carageniuncllem1  47055  iscnrm3rlem4  49524  aacllem  50382