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

Theorem difid 3845
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 3473 . 2  |-  A  C_  A
2 ssdif0 3835 . 2  |-  ( A 
C_  A  <->  ( A  \  A )  =  (/) )
31, 2mpbi 208 1  |-  ( A 
\  A )  =  (/)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1370    \ cdif 3423    C_ wss 3426   (/)c0 3735
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-v 3070  df-dif 3429  df-in 3433  df-ss 3440  df-nul 3736
This theorem is referenced by:  dif0  3847  difun2  3856  diftpsn3  4110  difxp1  5361  difxp2  5362  2oconcl  7043  oev2  7063  fin1a2lem13  8682  ruclem13  13626  strle1  14371  efgi1  16322  frgpuptinv  16372  dprdsn  16638  ablfac1eulem  16678  fctop  18724  cctop  18726  topcld  18755  indiscld  18811  mretopd  18812  restcld  18892  conndisj  19136  csdfil  19583  ufinffr  19618  prdsxmslem2  20220  bcth3  20958  voliunlem3  21149  uhgra0v  23379  usgra0v  23425  cusgra1v  23504  zrdivrng  24054  imadifxp  26073  difico  26207  0elsiga  26691  prsiga  26708  sibf0  26854  probun  26936  ballotlemfp1  27008  symdifid  27991  onint1  28429  compne  29834  frgra1v  30728  1vwmgra  30733  gsumdifsnd  30900  gsumdifsndf  30903
  Copyright terms: Public domain W3C validator