Theorem difid 4330

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

Syntax hints:   = wceq 1537   ∖ cdif 3933   ⊆ wss 3936  ∅c0 4291

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-dif 3939  df-in 3943  df-ss 3952  df-nul 4292

This theorem is referenced by:  dif0  4332  difun2  4429  diftpsn3  4735  symdifid  5009  difxp1  6022  difxp2  6023  2oconcl  8128  oev2  8148  fin1a2lem13  9834  ruclem13  15595  strle1  16592  efgi1  18847  frgpuptinv  18897  gsumdifsnd  19081  dprdsn  19158  ablfac1eulem  19194  fctop  21612  cctop  21614  topcld  21643  indiscld  21699  mretopd  21700  restcld  21780  conndisj  22024  csdfil  22502  ufinffr  22537  prdsxmslem2  23139  bcth3  23934  voliunlem3  24153  uhgr0vb  26857  uhgr0  26858  nbgr1vtx  27140  uvtx01vtx  27179  cplgr1v  27212  frgr1v  28050  1vwmgr  28055  difres  30350  imadifxp  30351  difico  30506  fzodif1  30516  symgcom2  30728  cycpmrn  30785  tocyccntz  30786  lindssn  30939  lbslsat  31014  0elsiga  31373  prsiga  31390  fiunelcarsg  31574  sibf0  31592  probun  31677  ballotlemfp1  31749  onint1  33797  poimirlem22  34929  poimirlem30  34937  zrdivrng  35246  ntrk0kbimka  40438  clsk3nimkb  40439  ntrclscls00  40465  ntrclskb  40468  ntrneicls11  40489  compne  40822  fzdifsuc2  41626  dvmptfprodlem  42278  fouriercn  42566  prsal  42652  caragenuncllem  42843  carageniuncllem1  42852  caratheodorylem1  42857  gsumdifsndf  44137