Theorem undif2 3816

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

Syntax hints:   = wceq 1437   \ cdif 3376   u. cun 3377

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-ral 2719  df-rab 2723  df-v 3024  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-nul 3705

This theorem is referenced by:  undif  3821  dfif5  3870  funiunfv  6112  difex2  6556  undom  7613  domss2  7684  sucdom2  7721  unfi  7791  marypha1lem  7900  kmlem11  8541  hashun2  12512  hashun3  12513  cvgcmpce  13821  dprd2da  17618  dpjcntz  17628  dpjdisj  17629  dpjlsm  17630  dpjidcl  17634  ablfac1eu  17649  dfcon2  20376  2ndcdisj2  20414  fixufil  20879  fin1aufil  20889  xrge0gsumle  21793  unmbl  22433  volsup  22451  mbfss  22544  itg2cnlem2  22662  iblss2  22705  amgm  23858  wilthlem2  23936  ftalem3  23941  rpvmasum2  24292  esumpad  28828  imadifss  31835  elrfi  35448  meaunle  38153