Theorem difid 3896

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 3522	. 2
2		ssdif0 3885	. 2
3	1, 2	mpbi 208	1

Syntax hints:  =wceq 1395  \cdif 3472  C_wss 3475  c0 3784

This theorem is referenced by:  dif0  3898  difun2  3907  diftpsn3  4168  difxp1  5437  difxp2  5438  2oconcl  7172  oev2  7192  fin1a2lem13  8813  ruclem13  13975  strle1  14728  efgi1  16739  frgpuptinv  16789  gsumdifsnd  16987  dprdsn  17083  ablfac1eulem  17123  fctop  19505  cctop  19507  topcld  19536  indiscld  19592  mretopd  19593  restcld  19673  conndisj  19917  csdfil  20395  ufinffr  20430  prdsxmslem2  21032  bcth3  21770  voliunlem3  21962  uhgra0v  24310  usgra0v  24371  cusgra1v  24461  frgra1v  24998  1vwmgra  25003  zrdivrng  25434  difres  27457  imadifxp  27458  difico  27594  0elsiga  28114  prsiga  28131  sibf0  28276  probun  28358  ballotlemfp1  28430  symdifid  29476  onint1  29914  compne  31349  fzdifsuc2  31512  dvmptfprodlem  31741  fouriercn  32015  uhg0v  32377  gsumdifsndf  32955

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-v 3111  df-dif 3478  df-in 3482  df-ss 3489  df-nul 3785