Theorem undif1 4451

Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4447). 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 4262	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵))
2		invdif 4254	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵)
3	2	uneq1i 4139	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∖ 𝐵) ∪ 𝐵)
4		uncom 4133	. . . . 5 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (V ∖ 𝐵))
5		unvdif 4450	. . . . 5 ⊢ (𝐵 ∪ (V ∖ 𝐵)) = V
6	4, 5	eqtri 2758	. . . 4 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = V
7	6	ineq2i 4192	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = ((𝐴 ∪ 𝐵) ∩ V)
8		inv1 4373	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ V) = (𝐴 ∪ 𝐵)
9	7, 8	eqtri 2758	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = (𝐴 ∪ 𝐵)
10	1, 3, 9	3eqtr3i 2766	1 ⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵)

Syntax hints:   = wceq 1540  Vcvv 3459   ∖ cdif 3923   ∪ cun 3924   ∩ cin 3925

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309

This theorem is referenced by:  undif2  4452  undifr  4458  unidif0  5330  sofld  6176  fresaun  6749  ralxpmap  8910  enp1ilem  9284  difinf  9321  pwfilem  9328  infdif  10222  fin23lem11  10331  fin1a2lem13  10426  axcclem  10471  ttukeylem1  10523  ttukeylem7  10529  fpwwe2lem12  10656  hashbclem  14470  incexclem  15852  ramub1lem1  17046  ramub1lem2  17047  isstruct2  17168  setsdm  17189  mrieqvlemd  17641  mreexmrid  17655  islbs3  21116  lbsextlem4  21122  basdif0  22891  bwth  23348  locfincmp  23464  cldsubg  24049  nulmbl2  25489  volinun  25499  limcdif  25829  ellimc2  25830  limcmpt2  25837  dvreslem  25862  dvaddbr  25892  dvmulbr  25893  dvmulbrOLD  25894  lhop  25973  plyeq0  26168  rlimcnp  26927  difeq  32499  ffsrn  32706  symgcom2  33095  esumpad2  34087  measunl  34247  subfacp1lem1  35201  cvmscld  35295  pibt2  37435  stoweidlem44  46073