Theorem difid 3902

Description: The difference between a class and itself is the empty set. Proposition 5.15 of [TakeutiZaring] p. 20. Also Theorem 32 of [Suppes] p. 28. (Contributed by NM, 22-Apr-2004.)

Assertion

Ref	Expression
difid	⊢ (𝐴 ∖ 𝐴) = ∅

Proof of Theorem difid

Step	Hyp	Ref	Expression
1		ssid 3587	. 2 ⊢ 𝐴 ⊆ 𝐴
2		ssdif0 3896	. 2 ⊢ (𝐴 ⊆ 𝐴 ↔ (𝐴 ∖ 𝐴) = ∅)
3	1, 2	mpbi 219	1 ⊢ (𝐴 ∖ 𝐴) = ∅

Syntax hints:   = wceq 1475   ∖ cdif 3537   ⊆ wss 3540  ∅c0 3874

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-dif 3543  df-in 3547  df-ss 3554  df-nul 3875

This theorem is referenced by:  dif0  3904  difun2  4000  diftpsn3  4273  diftpsn3OLD  4274  symdifid  4535  difxp1  5478  difxp2  5479  2oconcl  7470  oev2  7490  fin1a2lem13  9117  ruclem13  14810  strle1  15800  efgi1  17957  frgpuptinv  18007  gsumdifsnd  18183  dprdsn  18258  ablfac1eulem  18294  fctop  20618  cctop  20620  topcld  20649  indiscld  20705  mretopd  20706  restcld  20786  conndisj  21029  csdfil  21508  ufinffr  21543  prdsxmslem2  22144  bcth3  22936  voliunlem3  23127  uhgr0vb  25738  uhgr0  25739  uhgra0v  25839  usgra0v  25900  cusgra1v  25990  frgra1v  26525  1vwmgra  26530  difres  28795  imadifxp  28796  difico  28935  0elsiga  29504  prsiga  29521  fiunelcarsg  29705  sibf0  29723  probun  29808  ballotlemfp1  29880  onint1  31618  poimirlem22  32601  poimirlem30  32609  zrdivrng  32922  ntrk0kbimka  37357  clsk3nimkb  37358  ntrclscls00  37384  ntrclskb  37387  ntrneicls11  37408  compne  37665  fzdifsuc2  38466  dvmptfprodlem  38834  fouriercn  39125  prsal  39214  caragenuncllem  39402  carageniuncllem1  39411  caratheodorylem1  39416  nbgr1vtx  40580  uvtxa01vtx0  40623  cplgr1v  40652  frgr1v  41441  1vwmgr  41446  gsumdifsndf  41937