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

Theorem dif0 3526
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 3524 . . 3  |-  ( A 
\  A )  =  (/)
21difeq2i 3293 . 2  |-  ( A 
\  ( A  \  A ) )  =  ( A  \  (/) )
3 difdif 3304 . 2  |-  ( A 
\  ( A  \  A ) )  =  A
42, 3eqtr3i 2307 1  |-  ( A 
\  (/) )  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1624    \ cdif 3151   (/)c0 3457
This theorem is referenced by:  undifv  3530  dffv2  5554  2oconcl  6498  oe0m0  6515  oev2  6518  infdiffi  7354  cnfcom2lem  7400  m1bits  12626  mreexdomd  13546  efgi0  15024  vrgpinv  15073  frgpuptinv  15075  frgpnabllem1  15156  gsumval3  15186  gsumcllem  15188  dprddisj2  15269  0cld  16770  indiscld  16823  mretopd  16824  hauscmplem  17128  ptbasfi  17271  cfinfil  17583  csdfil  17584  filufint  17610  bcth3  18748  rembl  18893  volsup  18908  symdif0  23777  onint1  24296
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rab 2554  df-v 2792  df-dif 3157  df-in 3161  df-ss 3168  df-nul 3458
  Copyright terms: Public domain W3C validator