Theorem difundir 4246

Description: Distributive law for class difference. (Contributed by NM, 17-Aug-2004.)

Assertion

Ref	Expression
difundir	⊢ ((𝐴 ∪ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶))

Proof of Theorem difundir

Step	Hyp	Ref	Expression
1		indir 4241	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶)))
2		invdif 4234	. 2 ⊢ ((𝐴 ∪ 𝐵) ∩ (V ∖ 𝐶)) = ((𝐴 ∪ 𝐵) ∖ 𝐶)
3		invdif 4234	. . 3 ⊢ (𝐴 ∩ (V ∖ 𝐶)) = (𝐴 ∖ 𝐶)
4		invdif 4234	. . 3 ⊢ (𝐵 ∩ (V ∖ 𝐶)) = (𝐵 ∖ 𝐶)
5	3, 4	uneq12i 4127	. 2 ⊢ ((𝐴 ∩ (V ∖ 𝐶)) ∪ (𝐵 ∩ (V ∖ 𝐶))) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶))
6	1, 2, 5	3eqtr3i 2768	1 ⊢ ((𝐴 ∪ 𝐵) ∖ 𝐶) = ((𝐴 ∖ 𝐶) ∪ (𝐵 ∖ 𝐶))

Syntax hints:   = wceq 1542  Vcvv 3447   ∖ cdif 3911   ∪ cun 3912   ∩ cin 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3407  df-v 3449  df-dif 3917  df-un 3919  df-in 3921

This theorem is referenced by:  dfsymdif3  4262  difun2  4446  diftpsn3  4768  strleun  17041  setsfun0  17056  mreexmrid  17538  mreexexlem2d  17540  mvdco  19242  dprd2da  19836  dmdprdsplit2lem  19839  ablfac1eulem  19866  lbsextlem4  20682  opsrtoslem2  21501  nulmbl2  24938  uniioombllem3  24987  sltlpss  27280  ex-dif  29431  indifundif  31517  imadifxp  31587  fzodif1  31765  cycpmrn  32063  ballotlemfp1  33181  ballotlemgun  33214  onint1  34998  lindsadd  36145  lindsenlbs  36147  poimirlem2  36154  poimirlem6  36158  poimirlem7  36159  poimirlem8  36160  poimirlem22  36174  dvmptfprodlem  44287  fourierdlem102  44551  fourierdlem114  44563  caragenuncllem  44855  carageniuncllem1  44864