Theorem dif0 4273

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

Syntax hints:   = wceq 1543   ∖ cdif 3850  ∅c0 4223

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-rab 3060  df-v 3400  df-dif 3856  df-nul 4224

This theorem is referenced by:  unvdif  4375  disjdif2  4380  iinvdif  4974  symdif0  4979  dffv2  6784  2oconcl  8208  oe0m0  8225  oev2  8228  infdiffi  9251  cnfcom2lem  9294  m1bits  15962  mreexdomd  17106  efgi0  19064  vrgpinv  19113  frgpuptinv  19115  frgpnabllem1  19212  gsumval3  19246  gsumcllem  19247  dprddisj2  19380  0cld  21889  indiscld  21942  mretopd  21943  hauscmplem  22257  cfinfil  22744  csdfil  22745  filufint  22771  bcth3  24182  rembl  24391  volsup  24407  disjdifprg  30587  tocycf  31057  tocyc01  31058  prsiga  31765  sigapildsyslem  31795  sigapildsys  31796  sxbrsigalem3  31905  0elcarsg  31940  carsgclctunlem3  31953  new0  33744  onint1  34324  csbdif  35182  lindsdom  35457  ntrclscls00  41294  ntrclskb  41297  compne  41673  prsal  43477  saluni  43483  caragen0  43662  carageniuncllem1  43677  iscnrm3rlem4  45853  aacllem  46119