Theorem undif1 4442

Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4438). 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 4253	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵))
2		invdif 4245	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵)
3	2	uneq1i 4130	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∖ 𝐵) ∪ 𝐵)
4		uncom 4124	. . . . 5 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (V ∖ 𝐵))
5		unvdif 4441	. . . . 5 ⊢ (𝐵 ∪ (V ∖ 𝐵)) = V
6	4, 5	eqtri 2753	. . . 4 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = V
7	6	ineq2i 4183	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = ((𝐴 ∪ 𝐵) ∩ V)
8		inv1 4364	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ V) = (𝐴 ∪ 𝐵)
9	7, 8	eqtri 2753	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = (𝐴 ∪ 𝐵)
10	1, 3, 9	3eqtr3i 2761	1 ⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵)

Syntax hints:   = wceq 1540  Vcvv 3450   ∖ cdif 3914   ∪ cun 3915   ∩ cin 3916

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300

This theorem is referenced by:  undif2  4443  undifr  4449  unidif0  5318  sofld  6163  fresaun  6734  ralxpmap  8872  enp1ilem  9230  difinf  9267  pwfilem  9274  infdif  10168  fin23lem11  10277  fin1a2lem13  10372  axcclem  10417  ttukeylem1  10469  ttukeylem7  10475  fpwwe2lem12  10602  hashbclem  14424  incexclem  15809  ramub1lem1  17004  ramub1lem2  17005  isstruct2  17126  setsdm  17147  mrieqvlemd  17597  mreexmrid  17611  islbs3  21072  lbsextlem4  21078  basdif0  22847  bwth  23304  locfincmp  23420  cldsubg  24005  nulmbl2  25444  volinun  25454  limcdif  25784  ellimc2  25785  limcmpt2  25792  dvreslem  25817  dvaddbr  25847  dvmulbr  25848  dvmulbrOLD  25849  lhop  25928  plyeq0  26123  rlimcnp  26882  difeq  32454  ffsrn  32659  symgcom2  33048  esumpad2  34053  measunl  34213  subfacp1lem1  35173  cvmscld  35267  pibt2  37412  stoweidlem44  46049