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

Theorem dif0 3499
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 3497 . . 3  |-  ( A 
\  A )  =  (/)
21difeq2i 3266 . 2  |-  ( A 
\  ( A  \  A ) )  =  ( A  \  (/) )
3 difdif 3277 . 2  |-  ( A 
\  ( A  \  A ) )  =  A
42, 3eqtr3i 2280 1  |-  ( A 
\  (/) )  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1619    \ cdif 3124   (/)c0 3430
This theorem is referenced by:  undifv  3503  dffv2  5526  2oconcl  6470  oe0m0  6487  oev2  6490  infdiffi  7326  cnfcom2lem  7372  m1bits  12593  mreexdomd  13513  efgi0  14991  vrgpinv  15040  frgpuptinv  15042  frgpnabllem1  15123  gsumval3  15153  gsumcllem  15155  dprddisj2  15236  0cld  16737  indiscld  16790  mretopd  16791  hauscmplem  17095  ptbasfi  17238  cfinfil  17550  csdfil  17551  filufint  17577  bcth3  18715  rembl  18860  volsup  18875  symdif0  23744  onint1  24263
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 1927  ax-ext 2239
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 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ne 2423  df-ral 2523  df-rab 2527  df-v 2765  df-dif 3130  df-in 3134  df-ss 3141  df-nul 3431
  Copyright terms: Public domain W3C validator