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

Theorem difid 3535
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 3210 . 2  |-  A  C_  A
2 ssdif0 3526 . 2  |-  ( A 
C_  A  <->  ( A  \  A )  =  (/) )
31, 2mpbi 199 1  |-  ( A 
\  A )  =  (/)
Colors of variables: wff set class
Syntax hints:    = wceq 1632    \ cdif 3162    C_ wss 3165   (/)c0 3468
This theorem is referenced by:  dif0  3537  difun2  3546  diftpsn3  3772  difxp1  6170  difxp2  6171  2oconcl  6518  oev2  6538  fin1a2lem13  8054  ruclem13  12536  strle1  13255  efgi1  15046  frgpuptinv  15096  dprdsn  15287  ablfac1eulem  15323  fctop  16757  cctop  16759  topcld  16788  indiscld  16844  mretopd  16845  restcld  16919  conndisj  17158  csdfil  17605  ufinffr  17640  prdsxmslem2  18091  bcth3  18769  voliunlem3  18925  zrdivrng  21115  ballotlemfp1  23066  0elsiga  23490  prsiga  23507  probun  23637  symdifid  24441  onint1  24960  compne  27745  usgra0v  28251  cusgra1v  28296  frgra1v  28422  1vwmgra  28427
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-v 2803  df-dif 3168  df-in 3172  df-ss 3179  df-nul 3469
  Copyright terms: Public domain W3C validator