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

Theorem difid 3744
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 3372 . 2  |-  A  C_  A
2 ssdif0 3734 . 2  |-  ( A 
C_  A  <->  ( A  \  A )  =  (/) )
31, 2mpbi 208 1  |-  ( A 
\  A )  =  (/)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1364    \ cdif 3322    C_ wss 3325   (/)c0 3634
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 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-v 2972  df-dif 3328  df-in 3332  df-ss 3339  df-nul 3635
This theorem is referenced by:  dif0  3746  difun2  3755  diftpsn3  4009  difxp1  5260  difxp2  5261  2oconcl  6939  oev2  6959  fin1a2lem13  8577  ruclem13  13520  strle1  14265  efgi1  16211  frgpuptinv  16261  dprdsn  16523  ablfac1eulem  16563  fctop  18567  cctop  18569  topcld  18598  indiscld  18654  mretopd  18655  restcld  18735  conndisj  18979  csdfil  19426  ufinffr  19461  prdsxmslem2  20063  bcth3  20801  voliunlem3  20992  uhgra0v  23179  usgra0v  23225  cusgra1v  23304  zrdivrng  23854  imadifxp  25874  difico  26006  0elsiga  26493  prsiga  26510  sibf0  26650  probun  26732  ballotlemfp1  26804  symdifid  27786  onint1  28225  compne  29621  frgra1v  30515  1vwmgra  30520  gsumdifsnd  30679  gsumdifsndf  30682
  Copyright terms: Public domain W3C validator