Theorem undif2 3904

Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 3900). Part of proof of Corollary 6K of [Enderton] p. 144. (Contributed by NM, 19-May-1998.)

Assertion

Ref	Expression
undif2

Proof of Theorem undif2

Step	Hyp	Ref	Expression
1		uncom 3647	. 2
2		undif1 3903	. 2
3		uncom 3647	. 2
4	1, 2, 3	3eqtri 2490	1

Syntax hints:  =wceq 1395  \cdif 3472  u.cun 3473

This theorem is referenced by:  undif  3908  dfif5  3957  funiunfv  6160  difex2  6607  undom  7625  domss2  7696  sucdom2  7734  unfi  7807  marypha1lem  7913  kmlem11  8561  hashun2  12451  hashun3  12452  cvgcmpce  13632  dprd2da  17091  dpjcntz  17101  dpjdisj  17102  dpjlsm  17103  dpjidcl  17107  dpjidclOLD  17114  ablfac1eu  17124  dfcon2  19920  2ndcdisj2  19958  fixufil  20423  fin1aufil  20433  xrge0gsumle  21338  unmbl  21948  volsup  21966  mbfss  22053  itg2cnlem2  22169  iblss2  22212  amgm  23320  wilthlem2  23343  ftalem3  23348  rpvmasum2  23697  elrfi  30626

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