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

Theorem dif0 3524
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 3522 . . 3  |-  ( A 
\  A )  =  (/)
21difeq2i 3291 . 2  |-  ( A 
\  ( A  \  A ) )  =  ( A  \  (/) )
3 difdif 3302 . 2  |-  ( A 
\  ( A  \  A ) )  =  A
42, 3eqtr3i 2305 1  |-  ( A 
\  (/) )  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1623    \ cdif 3149   (/)c0 3455
This theorem is referenced by:  undifv  3528  dffv2  5592  2oconcl  6502  oe0m0  6519  oev2  6522  infdiffi  7358  cnfcom2lem  7404  m1bits  12631  mreexdomd  13551  efgi0  15029  vrgpinv  15078  frgpuptinv  15080  frgpnabllem1  15161  gsumval3  15191  gsumcllem  15193  dprddisj2  15274  0cld  16775  indiscld  16828  mretopd  16829  hauscmplem  17133  ptbasfi  17276  cfinfil  17588  csdfil  17589  filufint  17615  bcth3  18753  rembl  18898  volsup  18913  disjdifprg  23352  prsiga  23492  symdif0  24368  onint1  24888
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rab 2552  df-v 2790  df-dif 3155  df-in 3159  df-ss 3166  df-nul 3456
  Copyright terms: Public domain W3C validator