Theorem undif1 4187

Description: Absorption of difference by union. This decomposes a union into two disjoint classes (see disjdif 4184). 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 4019	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵))
2		invdif 4011	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐵)) = (𝐴 ∖ 𝐵)
3	2	uneq1i 3906	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐵)) ∪ 𝐵) = ((𝐴 ∖ 𝐵) ∪ 𝐵)
4		uncom 3900	. . . . 5 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = (𝐵 ∪ (V ∖ 𝐵))
5		unvdif 4186	. . . . 5 ⊢ (𝐵 ∪ (V ∖ 𝐵)) = V
6	4, 5	eqtri 2782	. . . 4 ⊢ ((V ∖ 𝐵) ∪ 𝐵) = V
7	6	ineq2i 3954	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = ((𝐴 ∪ 𝐵) ∩ V)
8		inv1 4113	. . 3 ⊢ ((𝐴 ∪ 𝐵) ∩ V) = (𝐴 ∪ 𝐵)
9	7, 8	eqtri 2782	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ ((V ∖ 𝐵) ∪ 𝐵)) = (𝐴 ∪ 𝐵)
10	1, 3, 9	3eqtr3i 2790	1 ⊢ ((𝐴 ∖ 𝐵) ∪ 𝐵) = (𝐴 ∪ 𝐵)

Syntax hints:   = wceq 1632  Vcvv 3340   ∖ cdif 3712   ∪ cun 3713   ∩ cin 3714

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059

This theorem is referenced by:  undif2  4188  unidif0  4987  pwundif  5171  sofld  5739  fresaun  6236  ralxpmap  8075  enp1ilem  8361  difinf  8397  pwfilem  8427  infdif  9243  fin23lem11  9351  fin1a2lem13  9446  axcclem  9491  ttukeylem1  9543  ttukeylem7  9549  fpwwe2lem13  9676  hashbclem  13448  incexclem  14787  ramub1lem1  15952  ramub1lem2  15953  isstruct2  16089  setsdm  16114  mrieqvlemd  16511  mreexmrid  16525  islbs3  19377  lbsextlem4  19383  basdif0  20979  bwth  21435  locfincmp  21551  cldsubg  22135  nulmbl2  23524  volinun  23534  limcdif  23859  ellimc2  23860  limcmpt2  23867  dvreslem  23892  dvaddbr  23920  dvmulbr  23921  lhop  23998  plyeq0  24186  rlimcnp  24912  difeq  29683  ffsrn  29834  esumpad2  30448  measunl  30609  subfacp1lem1  31489  cvmscld  31583  compneOLD  39164  stoweidlem44  40782