Theorem dif0 4334

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 4332	. . 3 ⊢ (𝐴 ∖ 𝐴) = ∅
2	1	difeq2i 4080	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = (𝐴 ∖ ∅)
3		difdif 4091	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = 𝐴
4	2, 3	eqtr3i 2790	1 ⊢ (𝐴 ∖ ∅) = 𝐴

Syntax hints:   = wceq 1563   ∖ cdif 3904  ∅c0 4288

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-dif 3910  df-nul 4289

This theorem is referenced by:  unvdif  4432  disjdif2  4437  csbdif  4482  iinvdif  5041  symdif0  5046  dffv2  6966  2oconcl  8476  oe0m0  8493  oev2  8496  infdiffi  9615  cnfcom2lem  9658  brttrcl2  9671  ttrcltr  9673  rnttrcl  9679  indconst0  12218  m1bits  16486  mreexdomd  17693  efgi0  19778  vrgpinv  19827  frgpuptinv  19829  frgpnabllem1  19931  gsumval3  19965  gsumcllem  19966  dprddisj2  20099  0cld  23152  indiscld  23205  mretopd  23206  hauscmplem  23520  cfinfil  24007  csdfil  24008  filufint  24034  bcth3  25447  rembl  25656  volsup  25672  new0  28011  disjdifprg  32826  tocycf  33345  tocyc01  33346  prsiga  34433  sigapildsyslem  34463  sigapildsys  34464  sxbrsigalem3  34574  0elcarsg  34609  carsgclctunlem3  34622  onint1  36817  lindsdom  38120  oe0rif  43869  tfsconcat0i  43929  ntrclscls00  44649  ntrclskb  44652  compne  45009  prsal  46891  saluni  46898  caragen0  47079  carageniuncllem1  47094  iscnrm3rlem4  49573  aacllem  50431