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

Theorem dif0 3430
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 3428 . . 3  |-  ( A 
\  A )  =  (/)
21difeq2i 3208 . 2  |-  ( A 
\  ( A  \  A ) )  =  ( A  \  (/) )
3 difdif 3219 . 2  |-  ( A 
\  ( A  \  A ) )  =  A
42, 3eqtr3i 2275 1  |-  ( A 
\  (/) )  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1619    \ cdif 3075   (/)c0 3362
This theorem is referenced by:  undifv  3434  dffv2  5444  2oconcl  6388  oe0m0  6405  oev2  6408  infdiffi  7242  cnfcom2lem  7288  m1bits  12505  efgi0  14864  vrgpinv  14913  frgpuptinv  14915  frgpnabllem1  14996  gsumval3  15026  gsumcllem  15028  dprddisj2  15109  0cld  16607  indiscld  16660  mretopd  16661  hauscmplem  16965  ptbasfi  17108  cfinfil  17420  csdfil  17421  filufint  17447  bcth3  18585  rembl  18730  volsup  18745  symdif0  23543  onint1  24062
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-ral 2513  df-rab 2516  df-v 2729  df-dif 3081  df-in 3085  df-ss 3089  df-nul 3363
  Copyright terms: Public domain W3C validator