Theorem undif2 3855

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

Assertion

Ref	Expression
undif2	|- ( A u. ( B \ A ) ) = ( A u. B )

Proof of Theorem undif2

Step	Hyp	Ref	Expression
1		uncom 3590	. 2 |- ( A u. ( B \ A ) ) = ( ( B \ A ) u. A )
2		undif1 3854	. 2 |- ( ( B \ A ) u. A ) = ( B u. A )
3		uncom 3590	. 2 |- ( B u. A ) = ( A u. B )
4	1, 2, 3	3eqtri 2488	1 |- ( A u. ( B \ A ) ) = ( A u. B )

Syntax hints:   = wceq 1455   \ cdif 3413   u. cun 3414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744

This theorem is referenced by:  undif  3860  dfif5  3909  funiunfv  6178  difex2  6625  undom  7686  domss2  7757  sucdom2  7794  unfi  7864  marypha1lem  7973  kmlem11  8616  hashun2  12594  hashun3  12595  cvgcmpce  13927  dprd2da  17724  dpjcntz  17734  dpjdisj  17735  dpjlsm  17736  dpjidcl  17740  ablfac1eu  17755  dfcon2  20483  2ndcdisj2  20521  fixufil  20986  fin1aufil  20996  xrge0gsumle  21900  unmbl  22540  volsup  22558  mbfss  22651  itg2cnlem2  22769  iblss2  22812  amgm  23965  wilthlem2  24043  ftalem3  24048  rpvmasum2  24399  esumpad  28925  imadifss  31973  elrfi  35581  meaunle  38340