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

Theorem difid 3899
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 3888 . 2  |-  ( A 
C_  A  <->  ( A  \  A )  =  (/) )
31, 2mpbi 208 1  |-  ( A 
\  A )  =  (/)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1395    \ cdif 3468    C_ wss 3471   (/)c0 3793
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-v 3111  df-dif 3474  df-in 3478  df-ss 3485  df-nul 3794
This theorem is referenced by:  dif0  3901  difun2  3910  diftpsn3  4170  symdifid  4411  difxp1  5439  difxp2  5440  2oconcl  7171  oev2  7191  fin1a2lem13  8809  ruclem13  13986  strle1  14742  efgi1  16865  frgpuptinv  16915  gsumdifsnd  17113  dprdsn  17209  ablfac1eulem  17249  fctop  19631  cctop  19633  topcld  19662  indiscld  19718  mretopd  19719  restcld  19799  conndisj  20042  csdfil  20520  ufinffr  20555  prdsxmslem2  21157  bcth3  21895  voliunlem3  22087  uhgra0v  24436  usgra0v  24497  cusgra1v  24587  frgra1v  25124  1vwmgra  25129  zrdivrng  25560  difres  27594  imadifxp  27595  difico  27746  0elsiga  28275  prsiga  28292  sibf0  28451  probun  28533  ballotlemfp1  28605  onint1  30076  compne  31511  fzdifsuc2  31673  dvmptfprodlem  31902  fouriercn  32176  uhg0v  32597  gsumdifsndf  33057
  Copyright terms: Public domain W3C validator