Theorem dif0 4098

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 4096	. . 3 ⊢ (𝐴 ∖ 𝐴) = ∅
2	1	difeq2i 3876	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = (𝐴 ∖ ∅)
3		difdif 3887	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = 𝐴
4	2, 3	eqtr3i 2795	1 ⊢ (𝐴 ∖ ∅) = 𝐴

Syntax hints:   = wceq 1631   ∖ cdif 3720  ∅c0 4063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rab 3070  df-v 3353  df-dif 3726  df-in 3730  df-ss 3737  df-nul 4064

This theorem is referenced by:  unvdif  4185  disjdif2  4190  iinvdif  4727  symdif0  4732  dffv2  6415  2oconcl  7741  oe0m0  7758  oev2  7761  infdiffi  8723  cnfcom2lem  8766  m1bits  15370  mreexdomd  16517  efgi0  18340  vrgpinv  18389  frgpuptinv  18391  frgpnabllem1  18483  gsumval3  18515  gsumcllem  18516  dprddisj2  18646  0cld  21063  indiscld  21116  mretopd  21117  hauscmplem  21430  cfinfil  21917  csdfil  21918  filufint  21944  bcth3  23347  rembl  23528  volsup  23544  disjdifprg  29726  prsiga  30534  sigapildsyslem  30564  sigapildsys  30565  sxbrsigalem3  30674  0elcarsg  30709  carsgclctunlem3  30722  onint1  32785  csbdif  33508  lindsdom  33736  ntrclscls00  38890  ntrclskb  38893  compne  39169  prsal  41052  saluni  41058  caragen0  41237  carageniuncllem1  41252  aacllem  43075