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

Theorem difid 3497
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 3172 . 2  |-  A  C_  A
2 ssdif0 3488 . 2  |-  ( A 
C_  A  <->  ( A  \  A )  =  (/) )
31, 2mpbi 201 1  |-  ( A 
\  A )  =  (/)
Colors of variables: wff set class
Syntax hints:    = wceq 1619    \ cdif 3124    C_ wss 3127   (/)c0 3430
This theorem is referenced by:  dif0  3499  difun2  3508  difxp1  6088  difxp2  6089  2oconcl  6470  oev2  6490  ruclem13  12482  strle1  13201  efgi1  14992  frgpuptinv  15042  dprdsn  15233  ablfac1eulem  15269  fctop  16703  cctop  16705  topcld  16734  indiscld  16790  mretopd  16791  restcld  16865  conndisj  17104  csdfil  17551  ufinffr  17586  prdsxmslem2  18037  bcth3  18715  voliunlem3  18871  zrdivrng  21059  ballotlemfp1  23011  symdifid  23746  onint1  24263  compne  27010
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 2239
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 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ne 2423  df-v 2765  df-dif 3130  df-in 3134  df-ss 3141  df-nul 3431
  Copyright terms: Public domain W3C validator