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

Theorem difid 3523
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 3198 . 2  |-  A  C_  A
2 ssdif0 3514 . 2  |-  ( A 
C_  A  <->  ( A  \  A )  =  (/) )
31, 2mpbi 201 1  |-  ( A 
\  A )  =  (/)
Colors of variables: wff set class
Syntax hints:    = wceq 1624    \ cdif 3150    C_ wss 3153   (/)c0 3456
This theorem is referenced by:  dif0  3525  difun2  3534  difxp1  6115  difxp2  6116  2oconcl  6497  oev2  6517  ruclem13  12514  strle1  13233  efgi1  15024  frgpuptinv  15074  dprdsn  15265  ablfac1eulem  15301  fctop  16735  cctop  16737  topcld  16766  indiscld  16822  mretopd  16823  restcld  16897  conndisj  17136  csdfil  17583  ufinffr  17618  prdsxmslem2  18069  bcth3  18747  voliunlem3  18903  zrdivrng  21091  ballotlemfp1  23043  symdifid  23778  onint1  24295  compne  27041
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-v 2791  df-dif 3156  df-in 3160  df-ss 3167  df-nul 3457
  Copyright terms: Public domain W3C validator