MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  difid Structured version   Unicode version

Theorem difid 3890
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  |-  ( A 
\  A )  =  (/)

Proof of Theorem difid
StepHypRef Expression
1 ssid 3518 . 2  |-  A  C_  A
2 ssdif0 3880 . 2  |-  ( A 
C_  A  <->  ( A  \  A )  =  (/) )
31, 2mpbi 208 1  |-  ( A 
\  A )  =  (/)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1374    \ cdif 3468    C_ wss 3471   (/)c0 3780
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-ne 2659  df-v 3110  df-dif 3474  df-in 3478  df-ss 3485  df-nul 3781
This theorem is referenced by:  dif0  3892  difun2  3901  diftpsn3  4160  difxp1  5425  difxp2  5426  2oconcl  7145  oev2  7165  fin1a2lem13  8783  ruclem13  13827  strle1  14577  efgi1  16530  frgpuptinv  16580  gsumdifsnd  16773  dprdsn  16868  ablfac1eulem  16908  fctop  19266  cctop  19268  topcld  19297  indiscld  19353  mretopd  19354  restcld  19434  conndisj  19678  csdfil  20125  ufinffr  20160  prdsxmslem2  20762  bcth3  21500  voliunlem3  21692  uhgra0v  23975  usgra0v  24035  cusgra1v  24125  frgra1v  24662  1vwmgra  24667  zrdivrng  25098  difres  27118  imadifxp  27119  difico  27250  0elsiga  27742  prsiga  27759  sibf0  27904  probun  27986  ballotlemfp1  28058  symdifid  29041  onint1  29479  compne  30884  fouriercn  31490  gsumdifsndf  31897
  Copyright terms: Public domain W3C validator