Theorem dif0 4327

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 4325	. . 3 ⊢ (𝐴 ∖ 𝐴) = ∅
2	1	difeq2i 4072	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = (𝐴 ∖ ∅)
3		difdif 4084	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = 𝐴
4	2, 3	eqtr3i 2758	1 ⊢ (𝐴 ∖ ∅) = 𝐴

Syntax hints:   = wceq 1541   ∖ cdif 3895  ∅c0 4282

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-nul 4283

This theorem is referenced by:  unvdif  4424  disjdif2  4429  csbdif  4475  iinvdif  5032  symdif0  5037  dffv2  6925  2oconcl  8426  oe0m0  8443  oev2  8446  infdiffi  9557  cnfcom2lem  9600  brttrcl2  9613  ttrcltr  9615  rnttrcl  9621  m1bits  16355  mreexdomd  17559  efgi0  19636  vrgpinv  19685  frgpuptinv  19687  frgpnabllem1  19789  gsumval3  19823  gsumcllem  19824  dprddisj2  19957  0cld  22956  indiscld  23009  mretopd  23010  hauscmplem  23324  cfinfil  23811  csdfil  23812  filufint  23838  bcth3  25261  rembl  25471  volsup  25487  new0  27822  disjdifprg  32559  indconst0  32848  tocycf  33095  tocyc01  33096  prsiga  34167  sigapildsyslem  34197  sigapildsys  34198  sxbrsigalem3  34308  0elcarsg  34343  carsgclctunlem3  34356  onint1  36516  lindsdom  37677  oe0rif  43405  tfsconcat0i  43465  ntrclscls00  44186  ntrclskb  44189  compne  44560  prsal  46443  saluni  46450  caragen0  46631  carageniuncllem1  46646  iscnrm3rlem4  49070  aacllem  49929