Theorem undif2 4188

Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4184). 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 3900	. 2 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = ((𝐵 ∖ 𝐴) ∪ 𝐴)
2		undif1 4187	. 2 ⊢ ((𝐵 ∖ 𝐴) ∪ 𝐴) = (𝐵 ∪ 𝐴)
3		uncom 3900	. 2 ⊢ (𝐵 ∪ 𝐴) = (𝐴 ∪ 𝐵)
4	1, 2, 3	3eqtri 2786	1 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵)

Syntax hints:   = wceq 1632   ∖ cdif 3712   ∪ cun 3713

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059

This theorem is referenced by:  undif  4193  dfif5  4246  funiunfv  6669  difex2  7134  undom  8213  domss2  8284  sucdom2  8321  unfi  8392  marypha1lem  8504  kmlem11  9174  hashun2  13364  hashun3  13365  cvgcmpce  14749  dprd2da  18641  dpjcntz  18651  dpjdisj  18652  dpjlsm  18653  dpjidcl  18657  ablfac1eu  18672  dfconn2  21424  2ndcdisj2  21462  fixufil  21927  fin1aufil  21937  xrge0gsumle  22837  unmbl  23505  volsup  23524  mbfss  23612  itg2cnlem2  23728  iblss2  23771  amgm  24916  wilthlem2  24994  ftalem3  25000  rpvmasum2  25400  esumpad  30426  noetalem3  32171  noetalem4  32172  imadifss  33697  elrfi  37759  meaunle  41184