Theorem difid 4244

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

Syntax hints:   = wceq 1520   ∖ cdif 3851   ⊆ wss 3854  ∅c0 4206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-ext 2767

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-v 3434  df-dif 3857  df-in 3861  df-ss 3869  df-nul 4207

This theorem is referenced by:  dif0  4246  difun2  4337  diftpsn3  4636  symdifid  4902  difxp1  5890  difxp2  5891  2oconcl  7970  oev2  7990  fin1a2lem13  9669  ruclem13  15416  strle1  16409  efgi1  18562  frgpuptinv  18612  gsumdifsnd  18789  dprdsn  18863  ablfac1eulem  18899  fctop  21284  cctop  21286  topcld  21315  indiscld  21371  mretopd  21372  restcld  21452  conndisj  21696  csdfil  22174  ufinffr  22209  prdsxmslem2  22810  bcth3  23605  voliunlem3  23824  uhgr0vb  26528  uhgr0  26529  nbgr1vtx  26811  uvtx01vtx  26850  cplgr1v  26883  frgr1v  27730  1vwmgr  27735  difres  30016  imadifxp  30017  difico  30166  fzodif1  30174  lindssn  30540  lbslsat  30573  0elsiga  30946  prsiga  30963  fiunelcarsg  31147  sibf0  31165  probun  31250  ballotlemfp1  31322  onint1  33350  poimirlem22  34391  poimirlem30  34399  zrdivrng  34709  ntrk0kbimka  39825  clsk3nimkb  39826  ntrclscls00  39852  ntrclskb  39855  ntrneicls11  39876  compne  40264  fzdifsuc2  41071  dvmptfprodlem  41724  fouriercn  42013  prsal  42099  caragenuncllem  42290  carageniuncllem1  42299  caratheodorylem1  42304  gsumdifsndf  43845