Theorem difid 4091

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

Syntax hints:   = wceq 1632   ∖ cdif 3712   ⊆ wss 3715  ∅c0 4058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-dif 3718  df-in 3722  df-ss 3729  df-nul 4059

This theorem is referenced by:  dif0  4093  difun2  4192  diftpsn3  4477  diftpsn3OLD  4478  symdifid  4751  difxp1  5717  difxp2  5718  2oconcl  7752  oev2  7772  fin1a2lem13  9426  ruclem13  15170  strle1  16175  efgi1  18334  frgpuptinv  18384  gsumdifsnd  18560  dprdsn  18635  ablfac1eulem  18671  fctop  21010  cctop  21012  topcld  21041  indiscld  21097  mretopd  21098  restcld  21178  conndisj  21421  csdfil  21899  ufinffr  21934  prdsxmslem2  22535  bcth3  23328  voliunlem3  23520  uhgr0vb  26166  uhgr0  26167  nbgr1vtx  26453  uvtx01vtx  26500  uvtxa01vtx0OLD  26502  cplgr1v  26536  frgr1v  27425  1vwmgr  27430  difres  29720  imadifxp  29721  difico  29854  0elsiga  30486  prsiga  30503  fiunelcarsg  30687  sibf0  30705  probun  30790  ballotlemfp1  30862  onint1  32754  poimirlem22  33744  poimirlem30  33752  zrdivrng  34065  ntrk0kbimka  38839  clsk3nimkb  38840  ntrclscls00  38866  ntrclskb  38869  ntrneicls11  38890  compne  39145  compneOLD  39146  fzdifsuc2  40023  dvmptfprodlem  40662  fouriercn  40952  prsal  41041  caragenuncllem  41232  carageniuncllem1  41241  caratheodorylem1  41246  gsumdifsndf  42654