Theorem dif0 4400

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 4398	. . 3 ⊢ (𝐴 ∖ 𝐴) = ∅
2	1	difeq2i 4146	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = (𝐴 ∖ ∅)
3		difdif 4158	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = 𝐴
4	2, 3	eqtr3i 2770	1 ⊢ (𝐴 ∖ ∅) = 𝐴

Syntax hints:   = wceq 1537   ∖ cdif 3973  ∅c0 4352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-nul 4353

This theorem is referenced by:  unvdif  4498  disjdif2  4503  csbdif  4547  iinvdif  5103  symdif0  5108  dffv2  7017  2oconcl  8559  oe0m0  8576  oev2  8579  infdiffi  9727  cnfcom2lem  9770  brttrcl2  9783  ttrcltr  9785  rnttrcl  9791  m1bits  16486  mreexdomd  17707  efgi0  19762  vrgpinv  19811  frgpuptinv  19813  frgpnabllem1  19915  gsumval3  19949  gsumcllem  19950  dprddisj2  20083  0cld  23067  indiscld  23120  mretopd  23121  hauscmplem  23435  cfinfil  23922  csdfil  23923  filufint  23949  bcth3  25384  rembl  25594  volsup  25610  new0  27931  disjdifprg  32597  tocycf  33110  tocyc01  33111  prsiga  34095  sigapildsyslem  34125  sigapildsys  34126  sxbrsigalem3  34237  0elcarsg  34272  carsgclctunlem3  34285  onint1  36415  lindsdom  37574  oe0rif  43247  tfsconcat0i  43307  ntrclscls00  44028  ntrclskb  44031  compne  44410  prsal  46239  saluni  46246  caragen0  46427  carageniuncllem1  46442  iscnrm3rlem4  48623  aacllem  48895