Theorem dif0 4384

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

Syntax hints:   = wceq 1537   ∖ cdif 3960  ∅c0 4339

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-nul 4340

This theorem is referenced by:  unvdif  4481  disjdif2  4486  csbdif  4530  iinvdif  5085  symdif0  5090  dffv2  7004  2oconcl  8540  oe0m0  8557  oev2  8560  infdiffi  9696  cnfcom2lem  9739  brttrcl2  9752  ttrcltr  9754  rnttrcl  9760  m1bits  16474  mreexdomd  17694  efgi0  19753  vrgpinv  19802  frgpuptinv  19804  frgpnabllem1  19906  gsumval3  19940  gsumcllem  19941  dprddisj2  20074  0cld  23062  indiscld  23115  mretopd  23116  hauscmplem  23430  cfinfil  23917  csdfil  23918  filufint  23944  bcth3  25379  rembl  25589  volsup  25605  new0  27928  disjdifprg  32595  tocycf  33120  tocyc01  33121  prsiga  34112  sigapildsyslem  34142  sigapildsys  34143  sxbrsigalem3  34254  0elcarsg  34289  carsgclctunlem3  34302  onint1  36432  lindsdom  37601  oe0rif  43275  tfsconcat0i  43335  ntrclscls00  44056  ntrclskb  44059  compne  44437  prsal  46274  saluni  46281  caragen0  46462  carageniuncllem1  46477  iscnrm3rlem4  48740  aacllem  49032