Theorem undif2 3903

Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 3899). 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 3648	. 2 |- ( A u. ( B \ A ) ) = ( ( B \ A ) u. A )
2		undif1 3902	. 2 |- ( ( B \ A ) u. A ) = ( B u. A )
3		uncom 3648	. 2 |- ( B u. A ) = ( A u. B )
4	1, 2, 3	3eqtri 2500	1 |- ( A u. ( B \ A ) ) = ( A u. B )

Syntax hints:   = wceq 1379   \ cdif 3473   u. cun 3474

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786

This theorem is referenced by:  undif  3907  dfif5  3955  funiunfv  6149  difex2  6592  undom  7606  domss2  7677  sucdom2  7715  unfi  7788  marypha1lem  7894  kmlem11  8541  hashun2  12420  hashun3  12421  cvgcmpce  13598  dprd2da  16905  dpjcntz  16915  dpjdisj  16916  dpjlsm  16917  dpjidcl  16921  dpjidclOLD  16928  ablfac1eu  16938  dfcon2  19726  2ndcdisj2  19764  fixufil  20250  fin1aufil  20260  xrge0gsumle  21165  unmbl  21775  volsup  21793  mbfss  21880  itg2cnlem2  21996  iblss2  22039  amgm  23145  wilthlem2  23168  ftalem3  23173  rpvmasum2  23522  elrfi  30457