Theorem undif2 4044

Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4040). Part of proof of Corollary 6K of [Enderton] p. 144. (Contributed by NM, 19-May-1998.)

Assertion

Ref	Expression
undif2	⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵)

Proof of Theorem undif2

Step	Hyp	Ref	Expression
1		uncom 3757	. 2 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = ((𝐵 ∖ 𝐴) ∪ 𝐴)
2		undif1 4043	. 2 ⊢ ((𝐵 ∖ 𝐴) ∪ 𝐴) = (𝐵 ∪ 𝐴)
3		uncom 3757	. 2 ⊢ (𝐵 ∪ 𝐴) = (𝐴 ∪ 𝐵)
4	1, 2, 3	3eqtri 2648	1 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵)

Syntax hints:   = wceq 1483   ∖ cdif 3571   ∪ cun 3572

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916

This theorem is referenced by:  undif  4049  dfif5  4102  funiunfv  6506  difex2  6969  undom  8048  domss2  8119  sucdom2  8156  unfi  8227  marypha1lem  8339  kmlem11  8982  hashun2  13172  hashun3  13173  cvgcmpce  14550  dprd2da  18441  dpjcntz  18451  dpjdisj  18452  dpjlsm  18453  dpjidcl  18457  ablfac1eu  18472  dfconn2  21222  2ndcdisj2  21260  fixufil  21726  fin1aufil  21736  xrge0gsumle  22636  unmbl  23305  volsup  23324  mbfss  23413  itg2cnlem2  23529  iblss2  23572  amgm  24717  wilthlem2  24795  ftalem3  24801  rpvmasum2  25201  esumpad  30117  noetalem3  31865  noetalem4  31866  imadifss  33384  elrfi  37257  meaunle  40681