Theorem dif0 4330

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

This proof depends on syntax axioms:   = wceq 1570   ∖ cdif 4048  ∅c0 4281

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-dif 4050  df-nul 4282

This theorem is used by:  unvdif  4432  disjdif2  4439  csbdif  4484  iinvdif  5045  symdif0  5050  dffv2  7011  2oconcl  8549  oe0m0  8566  oev2  8569  infdiffi  9696  cnfcom2lem  9739  brttrcl2  9752  ttrcltr  9754  rnttrcl  9760  indconst0  12372  m1bits  16654  mreexdomd  17873  efgi0  19985  vrgpinv  20034  frgpuptinv  20036  frgpnabllem1  20138  gsumval3  20172  gsumcllem  20173  dprddisj2  20306  lindsdom  22211  0cld  23411  indiscld  23464  mretopd  23465  hauscmplem  23779  cfinfil  24267  csdfil  24268  filufint  24294  bcth3  25707  rembl  25916  volsup  25932  new0  28307  disjdifprg  33267  tocycf  33777  tocyc01  33778  prsiga  34874  sigapildsyslem  34905  sigapildsys  34906  sxbrsigalem3  35015  0elcarsg  35050  carsgclctunlem3  35063  onint1  37452  oe0rif  44548  tfsconcat0i  44608  ntrclscls00  45327  ntrclskb  45330  compne  45684  prsal  47601  saluni  47608  caragen0  47789  carageniuncllem1  47804  iscnrm3rlem4  50388  aacllem  51367