Theorem undif1 4427

Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4423). 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 4238	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵))
2		invdif 4230	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵)
3	2	uneq1i 4115	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∖ 𝐵) ∪ 𝐵)
4		uncom 4109	. . . . 5 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (V ∖ 𝐵))
5		unvdif 4426	. . . . 5 ⊢ (𝐵 ∪ (V ∖ 𝐵)) = V
6	4, 5	eqtri 2752	. . . 4 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = V
7	6	ineq2i 4168	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = ((𝐴 ∪ 𝐵) ∩ V)
8		inv1 4349	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ V) = (𝐴 ∪ 𝐵)
9	7, 8	eqtri 2752	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = (𝐴 ∪ 𝐵)
10	1, 3, 9	3eqtr3i 2760	1 ⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵)

Syntax hints:   = wceq 1540  Vcvv 3436   ∖ cdif 3900   ∪ cun 3901   ∩ cin 3902

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285

This theorem is referenced by:  undif2  4428  undifr  4434  unidif0  5299  sofld  6136  fresaun  6695  ralxpmap  8823  enp1ilem  9167  difinf  9200  pwfilem  9207  infdif  10102  fin23lem11  10211  fin1a2lem13  10306  axcclem  10351  ttukeylem1  10403  ttukeylem7  10409  fpwwe2lem12  10536  hashbclem  14359  incexclem  15743  ramub1lem1  16938  ramub1lem2  16939  isstruct2  17060  setsdm  17081  mrieqvlemd  17535  mreexmrid  17549  islbs3  21062  lbsextlem4  21068  basdif0  22838  bwth  23295  locfincmp  23411  cldsubg  23996  nulmbl2  25435  volinun  25445  limcdif  25775  ellimc2  25776  limcmpt2  25783  dvreslem  25808  dvaddbr  25838  dvmulbr  25839  dvmulbrOLD  25840  lhop  25919  plyeq0  26114  rlimcnp  26873  difeq  32462  ffsrn  32672  symgcom2  33026  esumpad2  34023  measunl  34183  subfacp1lem1  35152  cvmscld  35246  pibt2  37391  stoweidlem44  46025