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 4071	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = (𝐴 ∖ ∅)
3		difdif 4082	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = 𝐴
4	2, 3	eqtr3i 2786	1 ⊢ (𝐴 ∖ ∅) = 𝐴

This proof depends on syntax axioms:   = wceq 1570   ∖ cdif 3896  ∅c0 4279

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-nul 4280

This theorem is used by:  unvdif  4429  disjdif2  4436  csbdif  4481  iinvdif  5040  symdif0  5045  dffv2  6978  2oconcl  8504  oe0m0  8521  oev2  8524  infdiffi  9652  cnfcom2lem  9695  brttrcl2  9708  ttrcltr  9710  rnttrcl  9716  indconst0  12325  m1bits  16603  mreexdomd  17816  efgi0  19927  vrgpinv  19976  frgpuptinv  19978  frgpnabllem1  20080  gsumval3  20114  gsumcllem  20115  dprddisj2  20248  lindsdom  22149  0cld  23349  indiscld  23402  mretopd  23403  hauscmplem  23717  cfinfil  24205  csdfil  24206  filufint  24232  bcth3  25645  rembl  25854  volsup  25870  new0  28243  disjdifprg  33162  tocycf  33671  tocyc01  33672  prsiga  34756  sigapildsyslem  34787  sigapildsys  34788  sxbrsigalem3  34897  0elcarsg  34932  carsgclctunlem3  34945  onint1  37217  oe0rif  44271  tfsconcat0i  44331  ntrclscls00  45051  ntrclskb  45054  compne  45409  prsal  47297  saluni  47304  caragen0  47485  carageniuncllem1  47500  iscnrm3rlem4  50020  aacllem  50908