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 2785	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 2732

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-nul 4280

This theorem is used by:  unvdif  4429  disjdif2  4436  csbdif  4481  iinvdif  5040  symdif0  5045  dffv2  6973  2oconcl  8490  oe0m0  8507  oev2  8510  infdiffi  9637  cnfcom2lem  9680  brttrcl2  9693  ttrcltr  9695  rnttrcl  9701  indconst0  12254  m1bits  16530  mreexdomd  17737  efgi0  19847  vrgpinv  19896  frgpuptinv  19898  frgpnabllem1  20000  gsumval3  20034  gsumcllem  20035  dprddisj2  20168  lindsdom  22063  0cld  23263  indiscld  23316  mretopd  23317  hauscmplem  23631  cfinfil  24119  csdfil  24120  filufint  24146  bcth3  25559  rembl  25768  volsup  25784  new0  28129  disjdifprg  33048  tocycf  33557  tocyc01  33558  prsiga  34641  sigapildsyslem  34672  sigapildsys  34673  sxbrsigalem3  34783  0elcarsg  34818  carsgclctunlem3  34831  onint1  37068  oe0rif  44126  tfsconcat0i  44186  ntrclscls00  44906  ntrclskb  44909  compne  45264  prsal  47146  saluni  47153  caragen0  47334  carageniuncllem1  47349  iscnrm3rlem4  49869  aacllem  50772