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

Theorem difid 3464
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 3139 . 2  |-  A  C_  A
2 ssdif0 3455 . 2  |-  ( A 
C_  A  <->  ( A  \  A )  =  (/) )
31, 2mpbi 201 1  |-  ( A 
\  A )  =  (/)
Colors of variables: wff set class
Syntax hints:    = wceq 1619    \ cdif 3091    C_ wss 3094   (/)c0 3397
This theorem is referenced by:  dif0  3466  difun2  3475  difxp1  6053  difxp2  6054  2oconcl  6435  oev2  6455  ruclem13  12447  strle1  13166  efgi1  14957  frgpuptinv  15007  dprdsn  15198  ablfac1eulem  15234  fctop  16668  cctop  16670  topcld  16699  indiscld  16755  mretopd  16756  restcld  16830  conndisj  17069  csdfil  17516  ufinffr  17551  prdsxmslem2  18002  bcth3  18680  voliunlem3  18836  zrdivrng  21024  ballotlemfp1  22976  symdifid  23711  onint1  24228  compne  26975
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-v 2742  df-dif 3097  df-in 3101  df-ss 3108  df-nul 3398
  Copyright terms: Public domain W3C validator