Theorem undif2 3664

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

Syntax hints:   = wceq 1649   \ cdif 3277   u. cun 3278

This theorem is referenced by:  undif  3668  dfif5  3711  difex2  4673  funiunfv  5954  undom  7155  domss2  7225  sucdom2  7262  unfi  7333  marypha1lem  7396  kmlem11  7996  hashun2  11612  hashun3  11613  cvgcmpce  12552  dprd2da  15555  dpjcntz  15565  dpjdisj  15566  dpjlsm  15567  dpjidcl  15571  ablfac1eu  15586  dfcon2  17435  2ndcdisj2  17473  fixufil  17907  fin1aufil  17917  xrge0gsumle  18817  unmbl  19385  volsup  19403  mbfss  19491  itg2cnlem2  19607  iblss2  19650  amgm  20782  wilthlem2  20805  ftalem3  20810  rpvmasum2  21159  elrfi  26638

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589