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

Theorem difun2 3699
 Description: Absorption of union by difference. Theorem 36 of [Suppes] p. 29. (Contributed by NM, 19-May-1998.)
Assertion
Ref Expression
difun2

Proof of Theorem difun2
StepHypRef Expression
1 difundir 3586 . 2
2 difid 3688 . . 3
32uneq2i 3490 . 2
4 un0 3644 . 2
51, 3, 43eqtri 2459 1
 Colors of variables: wff set class Syntax hints:   wceq 1652   cdif 3309   cun 3310  c0 3620 This theorem is referenced by:  uneqdifeq  3708  difprsn1  3927  orddif  4666  domunsncan  7199  elfiun  7426  hartogslem1  7500  cantnfp1lem3  7625  cda1dif  8045  infcda1  8062  ssxr  9134  dfn2  10223  incexclem  12604  mreexmrid  13856  lbsextlem4  16221  ufprim  17929  volun  19427  i1f1  19570  itgioo  19695  itgsplitioo  19717  plyeq0lem  20117  jensen  20815  difeq  23986  measun  24553  kelac2  27078  pwfi2f1o  27175 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621
 Copyright terms: Public domain W3C validator