Theorem undif1 4430

Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4426). Theorem 35 of [Suppes] p. 29. (Contributed by NM, 19-May-1998.)

Assertion

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

Proof of Theorem undif1

Step	Hyp	Ref	Expression
1		undir 4239	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵))
2		invdif 4231	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵)
3	2	uneq1i 4117	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∖ 𝐵) ∪ 𝐵)
4		uncom 4111	. . . . 5 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (V ∖ 𝐵))
5		unvdif 4429	. . . . 5 ⊢ (𝐵 ∪ (V ∖ 𝐵)) = V
6	4, 5	eqtri 2785	. . . 4 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = V
7	6	ineq2i 4169	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = ((𝐴 ∪ 𝐵) ∩ V)
8		inv1 4352	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ V) = (𝐴 ∪ 𝐵)
9	7, 8	eqtri 2785	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = (𝐴 ∪ 𝐵)
10	1, 3, 9	3eqtr3i 2793	1 ⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵)

Syntax hints:   = wceq 1560  Vcvv 3454   ∖ cdif 3901   ∪ cun 3902   ∩ cin 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286

This theorem is referenced by:  undif2  4431  undifr  4437  unidif0  5316  unidif0OLD  5317  sofld  6173  fresaun  6735  ralxpmap  8878  enp1ilem  9222  difinf  9255  pwfilem  9262  infdif  10164  fin23lem11  10274  fin1a2lem13  10369  axcclem  10414  ttukeylem1  10466  ttukeylem7  10472  fpwwe2lem12  10600  hashbclem  14465  incexclem  15866  ramub1lem1  17062  ramub1lem2  17063  isstruct2  17185  setsdm  17206  mrieqvlemd  17661  mreexmrid  17675  islbs3  21222  lbsextlem4  21228  basdif0  23010  bwth  23467  locfincmp  23583  cldsubg  24168  nulmbl2  25595  volinun  25605  limcdif  25935  ellimc2  25936  limcmpt2  25943  dvreslem  25968  dvaddbr  25997  dvmulbr  25998  lhop  26075  plyeq0  26268  rlimcnp  27027  difeq  32714  ffsrn  32927  symgcom2  33261  esumpad2  34350  measunl  34510  subfacp1lem1  35526  cvmscld  35620  pibt2  37908  stoweidlem44  46615