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

Theorem difid 3688
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 3359 . 2  |-  A  C_  A
2 ssdif0 3678 . 2  |-  ( A 
C_  A  <->  ( A  \  A )  =  (/) )
31, 2mpbi 200 1  |-  ( A 
\  A )  =  (/)
Colors of variables: wff set class
Syntax hints:    = wceq 1652    \ cdif 3309    C_ wss 3312   (/)c0 3620
This theorem is referenced by:  dif0  3690  difun2  3699  diftpsn3  3929  difxp1  6373  difxp2  6374  2oconcl  6739  oev2  6759  fin1a2lem13  8284  ruclem13  12833  strle1  13552  efgi1  15345  frgpuptinv  15395  dprdsn  15586  ablfac1eulem  15622  fctop  17060  cctop  17062  topcld  17091  indiscld  17147  mretopd  17148  restcld  17228  conndisj  17471  csdfil  17918  ufinffr  17953  prdsxmslem2  18551  bcth3  19276  voliunlem3  19438  uhgra0v  21337  usgra0v  21383  cusgra1v  21462  zrdivrng  22012  imadifxp  24030  difico  24138  0elsiga  24489  prsiga  24506  sibf0  24641  probun  24669  ballotlemfp1  24741  symdifid  25663  onint1  26191  compne  27610  frgra1v  28325  1vwmgra  28330
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-v 2950  df-dif 3315  df-in 3319  df-ss 3326  df-nul 3621
  Copyright terms: Public domain W3C validator