Theorem undif2 3886

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

Syntax hints:   = wceq 1381   \ cdif 3455   u. cun 3456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rab 2800  df-v 3095  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768

This theorem is referenced by:  undif  3890  dfif5  3938  funiunfv  6141  difex2  6588  undom  7603  domss2  7674  sucdom2  7712  unfi  7785  marypha1lem  7891  kmlem11  8538  hashun2  12425  hashun3  12426  cvgcmpce  13606  dprd2da  16959  dpjcntz  16969  dpjdisj  16970  dpjlsm  16971  dpjidcl  16975  dpjidclOLD  16982  ablfac1eu  16992  dfcon2  19786  2ndcdisj2  19824  fixufil  20289  fin1aufil  20299  xrge0gsumle  21204  unmbl  21814  volsup  21832  mbfss  21919  itg2cnlem2  22035  iblss2  22078  amgm  23185  wilthlem2  23208  ftalem3  23213  rpvmasum2  23562  elrfi  30594