Theorem undif2 3866

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

Syntax hints:   = wceq 1370   \ cdif 3436   u. cun 3437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-ral 2804  df-rab 2808  df-v 3080  df-dif 3442  df-un 3444  df-in 3446  df-ss 3453  df-nul 3749

This theorem is referenced by:  undif  3870  dfif5  3916  funiunfv  6077  difex2  6496  undom  7512  domss2  7583  sucdom2  7621  unfi  7693  marypha1lem  7797  kmlem11  8443  hashun2  12267  hashun3  12268  cvgcmpce  13402  dprd2da  16666  dpjcntz  16676  dpjdisj  16677  dpjlsm  16678  dpjidcl  16682  dpjidclOLD  16689  ablfac1eu  16699  dfcon2  19158  2ndcdisj2  19196  fixufil  19630  fin1aufil  19640  xrge0gsumle  20545  unmbl  21155  volsup  21173  mbfss  21260  itg2cnlem2  21376  iblss2  21419  amgm  22520  wilthlem2  22543  ftalem3  22548  rpvmasum2  22897  elrfi  29198