Theorem dif0 4220

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 4218	. . 3 ⊢ (𝐴 ∖ 𝐴) = ∅
2	1	difeq2i 3988	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = (𝐴 ∖ ∅)
3		difdif 3999	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = 𝐴
4	2, 3	eqtr3i 2804	1 ⊢ (𝐴 ∖ ∅) = 𝐴

Syntax hints:   = wceq 1507   ∖ cdif 3828  ∅c0 4180

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2750

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ral 3093  df-rab 3097  df-v 3417  df-dif 3834  df-in 3838  df-ss 3845  df-nul 4181

This theorem is referenced by:  unvdif  4307  disjdif2  4312  iinvdif  4869  symdif0  4874  dffv2  6586  2oconcl  7932  oe0m0  7949  oev2  7952  infdiffi  8917  cnfcom2lem  8960  m1bits  15652  mreexdomd  16781  efgi0  18607  vrgpinv  18658  frgpuptinv  18660  frgpnabllem1  18752  gsumval3  18784  gsumcllem  18785  dprddisj2  18914  0cld  21353  indiscld  21406  mretopd  21407  hauscmplem  21721  cfinfil  22208  csdfil  22209  filufint  22235  bcth3  23640  rembl  23847  volsup  23863  disjdifprg  30094  prsiga  31035  sigapildsyslem  31065  sigapildsys  31066  sxbrsigalem3  31175  0elcarsg  31210  carsgclctunlem3  31223  onint1  33317  csbdif  34048  lindsdom  34327  ntrclscls00  39779  ntrclskb  39782  compne  40191  prsal  42035  saluni  42041  caragen0  42220  carageniuncllem1  42235  aacllem  44270