Theorem difid 3901

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

Syntax hints:   = wceq 1474   ∖ cdif 3536   ⊆ wss 3539  ∅c0 3873

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-dif 3542  df-in 3546  df-ss 3553  df-nul 3874

This theorem is referenced by:  dif0  3903  difun2  3999  diftpsn3  4272  diftpsn3OLD  4273  symdifid  4529  difxp1  5463  difxp2  5464  2oconcl  7447  oev2  7467  fin1a2lem13  9094  ruclem13  14758  strle1  15748  efgi1  17905  frgpuptinv  17955  gsumdifsnd  18131  dprdsn  18206  ablfac1eulem  18242  fctop  20565  cctop  20567  topcld  20596  indiscld  20652  mretopd  20653  restcld  20733  conndisj  20976  csdfil  21455  ufinffr  21490  prdsxmslem2  22091  bcth3  22880  voliunlem3  23071  uhgra0v  25632  usgra0v  25693  cusgra1v  25783  frgra1v  26318  1vwmgra  26323  difres  28588  imadifxp  28589  difico  28728  0elsiga  29297  prsiga  29314  fiunelcarsg  29498  sibf0  29516  probun  29601  ballotlemfp1  29673  onint1  31411  poimirlem22  32384  poimirlem30  32392  zrdivrng  32705  ntrk0kbimka  37140  clsk3nimkb  37141  ntrclscls00  37167  ntrclskb  37170  ntrneicls11  37191  compne  37448  fzdifsuc2  38249  dvmptfprodlem  38617  fouriercn  38908  prsal  38997  caragenuncllem  39185  carageniuncllem1  39194  caratheodorylem1  39199  uhgr0vb  40278  uhgr0  40279  nbgr1vtx  40561  uvtxa01vtx0  40604  cplgr1v  40633  frgr1v  41422  1vwmgr  41427  gsumdifsndf  41918