Theorem dif0 4334

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 4332	. . 3 ⊢ (𝐴 ∖ 𝐴) = ∅
2	1	difeq2i 4078	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = (𝐴 ∖ ∅)
3		difdif 4089	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = 𝐴
4	2, 3	eqtr3i 2790	1 ⊢ (𝐴 ∖ ∅) = 𝐴

This proof depends on syntax axioms:   = wceq 1570   ∖ cdif 3903  ∅c0 4286

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-nul 4287

This theorem is used by:  unvdif  4436  disjdif2  4443  csbdif  4488  iinvdif  5048  symdif0  5053  dffv2  6980  2oconcl  8490  oe0m0  8507  oev2  8510  infdiffi  9630  cnfcom2lem  9673  brttrcl2  9686  ttrcltr  9688  rnttrcl  9694  indconst0  12241  m1bits  16515  mreexdomd  17722  efgi0  19813  vrgpinv  19862  frgpuptinv  19864  frgpnabllem1  19966  gsumval3  20000  gsumcllem  20001  dprddisj2  20134  0cld  23224  indiscld  23277  mretopd  23278  hauscmplem  23592  cfinfil  24079  csdfil  24080  filufint  24106  bcth3  25519  rembl  25728  volsup  25744  new0  28086  disjdifprg  32949  tocycf  33460  tocyc01  33461  prsiga  34544  sigapildsyslem  34575  sigapildsys  34576  sxbrsigalem3  34686  0elcarsg  34721  carsgclctunlem3  34734  onint1  36993  lindsdom  38298  oe0rif  44045  tfsconcat0i  44105  ntrclscls00  44825  ntrclskb  44828  compne  45183  prsal  47065  saluni  47072  caragen0  47253  carageniuncllem1  47268  iscnrm3rlem4  49754  aacllem  50654