Theorem difid 3948

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

Syntax hints:   = wceq 1483   ∖ cdif 3571   ⊆ wss 3574  ∅c0 3915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-dif 3577  df-in 3581  df-ss 3588  df-nul 3916

This theorem is referenced by:  dif0  3950  difun2  4048  diftpsn3  4332  diftpsn3OLD  4333  symdifid  4599  difxp1  5559  difxp2  5560  2oconcl  7583  oev2  7603  fin1a2lem13  9234  ruclem13  14971  strle1  15973  efgi1  18134  frgpuptinv  18184  gsumdifsnd  18360  dprdsn  18435  ablfac1eulem  18471  fctop  20808  cctop  20810  topcld  20839  indiscld  20895  mretopd  20896  restcld  20976  conndisj  21219  csdfil  21698  ufinffr  21733  prdsxmslem2  22334  bcth3  23128  voliunlem3  23320  uhgr0vb  25967  uhgr0  25968  nbgr1vtx  26254  uvtxa01vtx0  26297  cplgr1v  26326  frgr1v  27135  1vwmgr  27140  difres  29413  imadifxp  29414  difico  29545  0elsiga  30177  prsiga  30194  fiunelcarsg  30378  sibf0  30396  probun  30481  ballotlemfp1  30553  onint1  32448  poimirlem22  33431  poimirlem30  33439  zrdivrng  33752  ntrk0kbimka  38337  clsk3nimkb  38338  ntrclscls00  38364  ntrclskb  38367  ntrneicls11  38388  compne  38643  compneOLD  38644  fzdifsuc2  39525  dvmptfprodlem  40159  fouriercn  40449  prsal  40538  caragenuncllem  40726  carageniuncllem1  40735  caratheodorylem1  40740  gsumdifsndf  42144