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

Theorem dif0 3884
Description: The difference between a class and the empty set. Part of Exercise 4.4 of [Stoll] p. 16. (Contributed by NM, 17-Aug-2004.)
Assertion
Ref Expression
dif0  |-  ( A 
\  (/) )  =  A

Proof of Theorem dif0
StepHypRef Expression
1 difid 3882 . . 3  |-  ( A 
\  A )  =  (/)
21difeq2i 3604 . 2  |-  ( A 
\  ( A  \  A ) )  =  ( A  \  (/) )
3 difdif 3615 . 2  |-  ( A 
\  ( A  \  A ) )  =  A
42, 3eqtr3i 2474 1  |-  ( A 
\  (/) )  =  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1383    \ cdif 3458   (/)c0 3770
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rab 2802  df-v 3097  df-dif 3464  df-in 3468  df-ss 3475  df-nul 3771
This theorem is referenced by:  unvdif  3888  iinvdif  4387  dffv2  5931  2oconcl  7155  oe0m0  7172  oev2  7175  infdiffi  8077  cnfcom2lem  8148  cnfcom2lemOLD  8156  m1bits  14072  mreexdomd  15028  efgi0  16717  vrgpinv  16766  frgpuptinv  16768  frgpnabllem1  16856  gsumval3OLD  16887  gsumval3  16890  gsumcllem  16891  gsumcllemOLD  16892  dprddisj2  17066  dprddisj2OLD  17067  0cld  19517  indiscld  19570  mretopd  19571  hauscmplem  19884  ptbasfi  20060  cfinfil  20372  csdfil  20373  filufint  20399  bcth3  21748  rembl  21929  volsup  21944  disjdifprg  27414  prsiga  28109  sxbrsigalem3  28221  symdif0  29450  onint1  29890  dvmptfprodlem  31695  bj-disjdif  34394
  Copyright terms: Public domain W3C validator