Theorem undif1 4421

Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4418). 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 4250	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵))
2		invdif 4242	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵)
3	2	uneq1i 4132	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∖ 𝐵) ∪ 𝐵)
4		uncom 4126	. . . . 5 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (V ∖ 𝐵))
5		unvdif 4420	. . . . 5 ⊢ (𝐵 ∪ (V ∖ 𝐵)) = V
6	4, 5	eqtri 2843	. . . 4 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = V
7	6	ineq2i 4183	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = ((𝐴 ∪ 𝐵) ∩ V)
8		inv1 4345	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ V) = (𝐴 ∪ 𝐵)
9	7, 8	eqtri 2843	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = (𝐴 ∪ 𝐵)
10	1, 3, 9	3eqtr3i 2851	1 ⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵)

Syntax hints:   = wceq 1536  Vcvv 3493   ∖ cdif 3930   ∪ cun 3931   ∩ cin 3932

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2792

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2799  df-cleq 2813  df-clel 2892  df-nfc 2962  df-rab 3146  df-v 3495  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289

This theorem is referenced by:  undif2  4422  unidif0  5257  pwundifOLD  5454  sofld  6041  fresaun  6546  ralxpmap  8457  enp1ilem  8749  difinf  8785  pwfilem  8815  infdif  9628  fin23lem11  9736  fin1a2lem13  9831  axcclem  9876  ttukeylem1  9928  ttukeylem7  9934  fpwwe2lem13  10061  hashbclem  13808  incexclem  15187  ramub1lem1  16358  ramub1lem2  16359  isstruct2  16489  setsdm  16513  mrieqvlemd  16896  mreexmrid  16910  islbs3  19923  lbsextlem4  19929  basdif0  21557  bwth  22014  locfincmp  22130  cldsubg  22715  nulmbl2  24133  volinun  24143  limcdif  24472  ellimc2  24473  limcmpt2  24480  dvreslem  24505  dvaddbr  24533  dvmulbr  24534  lhop  24611  plyeq0  24799  rlimcnp  25541  difeq  30280  ffsrn  30465  symgcom2  30749  esumpad2  31339  measunl  31499  subfacp1lem1  32450  cvmscld  32544  pibt2  34725  stoweidlem44  42403