Theorem dif0 4313

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 4311	. . 3 ⊢ (𝐴 ∖ 𝐴) = ∅
2	1	difeq2i 4061	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = (𝐴 ∖ ∅)
3		difdif 4072	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = 𝐴
4	2, 3	eqtr3i 2765	1 ⊢ (𝐴 ∖ ∅) = 𝐴

Syntax hints:   = wceq 1547   ∖ cdif 3887  ∅c0 4268

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-nul 4269

This theorem is referenced by:  unvdif  4410  disjdif2  4415  csbdif  4460  iinvdif  5016  symdif0  5021  dffv2  6929  2oconcl  8435  oe0m0  8452  oev2  8455  infdiffi  9577  cnfcom2lem  9620  brttrcl2  9633  ttrcltr  9635  rnttrcl  9641  indconst0  12169  m1bits  16407  mreexdomd  17613  efgi0  19693  vrgpinv  19742  frgpuptinv  19744  frgpnabllem1  19846  gsumval3  19880  gsumcllem  19881  dprddisj2  20014  0cld  23028  indiscld  23081  mretopd  23082  hauscmplem  23396  cfinfil  23883  csdfil  23884  filufint  23910  bcth3  25323  rembl  25532  volsup  25548  new0  27881  disjdifprg  32671  tocycf  33205  tocyc01  33206  prsiga  34322  sigapildsyslem  34352  sigapildsys  34353  sxbrsigalem3  34463  0elcarsg  34498  carsgclctunlem3  34511  onint1  36684  lindsdom  37988  oe0rif  43737  tfsconcat0i  43797  ntrclscls00  44517  ntrclskb  44520  compne  44891  prsal  46768  saluni  46775  caragen0  46956  carageniuncllem1  46971  iscnrm3rlem4  49440  aacllem  50298