Theorem dif0 4326

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 4324	. . 3 ⊢ (𝐴 ∖ 𝐴) = ∅
2	1	difeq2i 4060	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = (𝐴 ∖ ∅)
3		difdif 4071	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = 𝐴
4	2, 3	eqtr3i 2785	1 ⊢ (𝐴 ∖ ∅) = 𝐴

This proof depends on syntax axioms:   = wceq 1569   ∖ cdif 4045  ∅c0 4278

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 4047  df-nul 4279

This theorem is used by:  unvdif  4428  disjdif2  4435  csbdif  4480  iinvdif  5039  symdif0  5044  dffv2  6981  2oconcl  8515  oe0m0  8532  oev2  8535  infdiffi  9663  cnfcom2lem  9706  brttrcl2  9719  ttrcltr  9721  rnttrcl  9727  indconst0  12336  m1bits  16616  mreexdomd  17829  efgi0  19940  vrgpinv  19989  frgpuptinv  19991  frgpnabllem1  20093  gsumval3  20127  gsumcllem  20128  dprddisj2  20261  lindsdom  22162  0cld  23362  indiscld  23415  mretopd  23416  hauscmplem  23730  cfinfil  24218  csdfil  24219  filufint  24245  bcth3  25658  rembl  25867  volsup  25883  new0  28256  disjdifprg  33217  tocycf  33725  tocyc01  33726  prsiga  34810  sigapildsyslem  34841  sigapildsys  34842  sxbrsigalem3  34951  0elcarsg  34986  carsgclctunlem3  34999  onint1  37330  oe0rif  44381  tfsconcat0i  44441  ntrclscls00  45160  ntrclskb  45163  compne  45518  prsal  47422  saluni  47429  caragen0  47610  carageniuncllem1  47625  iscnrm3rlem4  50151  aacllem  51108