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

Theorem difun2 3907
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 3750 . 2
2 difid 3896 . . 3
32uneq2i 3654 . 2
4 un0 3810 . 2
51, 3, 43eqtri 2490 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1395  \cdif 3472  u.cun 3473   c0 3784
This theorem is referenced by:  uneqdifeq  3916  difprsn1  4166  orddif  4976  domunsncan  7637  elfiun  7910  hartogslem1  7988  cantnfp1lem3  8120  cantnfp1lem3OLD  8146  cda1dif  8577  infcda1  8594  ssxr  9675  dfn2  10833  incexclem  13648  mreexmrid  15040  lbsextlem4  17807  ufprim  20410  volun  21955  i1f1  22097  itgioo  22222  itgsplitioo  22244  plyeq0lem  22607  jensen  23318  difeq  27416  measun  28182  elmrsubrn  28880  mrsubvrs  28882  finixpnum  30038  asindmre  30102  kelac2  31011  pwfi2f1o  31044  iccdifioo  31555  iccdifprioo  31556
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785
  Copyright terms: Public domain W3C validator