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

Theorem difid 3428
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 3118 . 2  |-  A  C_  A
2 ssdif0 3420 . 2  |-  ( A 
C_  A  <->  ( A  \  A )  =  (/) )
31, 2mpbi 201 1  |-  ( A 
\  A )  =  (/)
Colors of variables: wff set class
Syntax hints:    = wceq 1619    \ cdif 3075    C_ wss 3078   (/)c0 3362
This theorem is referenced by:  dif0  3430  difun2  3439  difxp1  6006  difxp2  6007  2oconcl  6388  oev2  6408  ruclem13  12394  strle1  13113  efgi1  14865  frgpuptinv  14915  dprdsn  15106  ablfac1eulem  15142  fctop  16573  cctop  16575  topcld  16604  indiscld  16660  mretopd  16661  restcld  16735  conndisj  16974  csdfil  17421  ufinffr  17456  prdsxmslem2  17907  bcth3  18585  voliunlem3  18741  zrdivrng  20929  symdifid  23545  onint1  24062  compne  26809
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 1926  ax-ext 2234
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 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-v 2729  df-dif 3081  df-in 3085  df-ss 3089  df-nul 3363
  Copyright terms: Public domain W3C validator