Theorem difid 3981

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 3657	. 2 ⊢ 𝐴 ⊆ 𝐴
2		ssdif0 3975	. 2 ⊢ (𝐴 ⊆ 𝐴 ↔ (𝐴 ∖ 𝐴) = ∅)
3	1, 2	mpbi 220	1 ⊢ (𝐴 ∖ 𝐴) = ∅

Syntax hints:   = wceq 1523   ∖ cdif 3604   ⊆ wss 3607  ∅c0 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-dif 3610  df-in 3614  df-ss 3621  df-nul 3949

This theorem is referenced by:  dif0  3983  difun2  4081  diftpsn3  4364  diftpsn3OLD  4365  symdifid  4631  difxp1  5594  difxp2  5595  2oconcl  7628  oev2  7648  fin1a2lem13  9272  ruclem13  15015  strle1  16020  efgi1  18180  frgpuptinv  18230  gsumdifsnd  18406  dprdsn  18481  ablfac1eulem  18517  fctop  20856  cctop  20858  topcld  20887  indiscld  20943  mretopd  20944  restcld  21024  conndisj  21267  csdfil  21745  ufinffr  21780  prdsxmslem2  22381  bcth3  23174  voliunlem3  23366  uhgr0vb  26012  uhgr0  26013  nbgr1vtx  26299  uvtx01vtx  26346  uvtxa01vtx0OLD  26348  cplgr1v  26382  frgr1v  27251  1vwmgr  27256  difres  29539  imadifxp  29540  difico  29673  0elsiga  30305  prsiga  30322  fiunelcarsg  30506  sibf0  30524  probun  30609  ballotlemfp1  30681  onint1  32573  poimirlem22  33561  poimirlem30  33569  zrdivrng  33882  ntrk0kbimka  38654  clsk3nimkb  38655  ntrclscls00  38681  ntrclskb  38684  ntrneicls11  38705  compne  38960  compneOLD  38961  fzdifsuc2  39838  dvmptfprodlem  40477  fouriercn  40767  prsal  40856  caragenuncllem  41047  carageniuncllem1  41056  caratheodorylem1  41061  gsumdifsndf  42469