Theorem dif0 4344

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 4342	. . 3 ⊢ (𝐴 ∖ 𝐴) = ∅
2	1	difeq2i 4089	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = (𝐴 ∖ ∅)
3		difdif 4101	. 2 ⊢ (𝐴 ∖ (𝐴 ∖ 𝐴)) = 𝐴
4	2, 3	eqtr3i 2755	1 ⊢ (𝐴 ∖ ∅) = 𝐴

Syntax hints:   = wceq 1540   ∖ cdif 3914  ∅c0 4299

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-nul 4300

This theorem is referenced by:  unvdif  4441  disjdif2  4446  csbdif  4490  iinvdif  5047  symdif0  5052  dffv2  6959  2oconcl  8470  oe0m0  8487  oev2  8490  infdiffi  9618  cnfcom2lem  9661  brttrcl2  9674  ttrcltr  9676  rnttrcl  9682  m1bits  16417  mreexdomd  17617  efgi0  19657  vrgpinv  19706  frgpuptinv  19708  frgpnabllem1  19810  gsumval3  19844  gsumcllem  19845  dprddisj2  19978  0cld  22932  indiscld  22985  mretopd  22986  hauscmplem  23300  cfinfil  23787  csdfil  23788  filufint  23814  bcth3  25238  rembl  25448  volsup  25464  new0  27793  disjdifprg  32511  tocycf  33081  tocyc01  33082  prsiga  34128  sigapildsyslem  34158  sigapildsys  34159  sxbrsigalem3  34270  0elcarsg  34305  carsgclctunlem3  34318  onint1  36444  lindsdom  37615  oe0rif  43281  tfsconcat0i  43341  ntrclscls00  44062  ntrclskb  44065  compne  44437  prsal  46323  saluni  46330  caragen0  46511  carageniuncllem1  46526  iscnrm3rlem4  48935  aacllem  49794