Theorem dif0 4335

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 4333	. . 3 ⊢ (𝐴 ∖ 𝐴) = ∅
2	1	difeq2i 4079	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = (𝐴 ∖ ∅)
3		difdif 4090	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = 𝐴
4	2, 3	eqtr3i 2788	1 ⊢ (𝐴 ∖ ∅) = 𝐴

Syntax hints:   = wceq 1570   ∖ cdif 3903  ∅c0 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-nul 4288

This theorem is referenced by:  unvdif  4437  disjdif2  4442  csbdif  4487  iinvdif  5047  symdif0  5052  dffv2  6978  2oconcl  8489  oe0m0  8506  oev2  8509  infdiffi  9628  cnfcom2lem  9671  brttrcl2  9684  ttrcltr  9686  rnttrcl  9692  indconst0  12231  m1bits  16499  mreexdomd  17706  efgi0  19791  vrgpinv  19840  frgpuptinv  19842  frgpnabllem1  19944  gsumval3  19978  gsumcllem  19979  dprddisj2  20112  0cld  23176  indiscld  23229  mretopd  23230  hauscmplem  23544  cfinfil  24031  csdfil  24032  filufint  24058  bcth3  25471  rembl  25680  volsup  25696  new0  28038  disjdifprg  32901  tocycf  33418  tocyc01  33419  prsiga  34502  sigapildsyslem  34532  sigapildsys  34533  sxbrsigalem3  34643  0elcarsg  34678  carsgclctunlem3  34691  onint1  36941  lindsdom  38246  oe0rif  43995  tfsconcat0i  44055  ntrclscls00  44775  ntrclskb  44778  compne  45133  prsal  47015  saluni  47022  caragen0  47203  carageniuncllem1  47218  iscnrm3rlem4  49704  aacllem  50584