NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  difdifdir GIF version

Theorem difdifdir 3637
Description: Distributive law for class difference. Exercise 4.8 of [Stoll] p. 16. (Contributed by NM, 18-Aug-2004.)
Assertion
Ref Expression
difdifdir ((A B) C) = ((A C) (B C))

Proof of Theorem difdifdir
StepHypRef Expression
1 dif32 3517 . . . . 5 ((A B) C) = ((A C) B)
2 invdif 3496 . . . . 5 ((A C) ∩ (V B)) = ((A C) B)
31, 2eqtr4i 2376 . . . 4 ((A B) C) = ((A C) ∩ (V B))
4 un0 3575 . . . 4 (((A C) ∩ (V B)) ∪ ) = ((A C) ∩ (V B))
53, 4eqtr4i 2376 . . 3 ((A B) C) = (((A C) ∩ (V B)) ∪ )
6 indi 3501 . . . 4 ((A C) ∩ ((V B) ∪ C)) = (((A C) ∩ (V B)) ∪ ((A C) ∩ C))
7 disjdif 3622 . . . . . 6 (C ∩ (A C)) =
8 incom 3448 . . . . . 6 (C ∩ (A C)) = ((A C) ∩ C)
97, 8eqtr3i 2375 . . . . 5 = ((A C) ∩ C)
109uneq2i 3415 . . . 4 (((A C) ∩ (V B)) ∪ ) = (((A C) ∩ (V B)) ∪ ((A C) ∩ C))
116, 10eqtr4i 2376 . . 3 ((A C) ∩ ((V B) ∪ C)) = (((A C) ∩ (V B)) ∪ )
125, 11eqtr4i 2376 . 2 ((A B) C) = ((A C) ∩ ((V B) ∪ C))
13 ddif 3398 . . . . 5 (V (V C)) = C
1413uneq2i 3415 . . . 4 ((V B) ∪ (V (V C))) = ((V B) ∪ C)
15 indm 3513 . . . . 5 (V (B ∩ (V C))) = ((V B) ∪ (V (V C)))
16 invdif 3496 . . . . . 6 (B ∩ (V C)) = (B C)
1716difeq2i 3382 . . . . 5 (V (B ∩ (V C))) = (V (B C))
1815, 17eqtr3i 2375 . . . 4 ((V B) ∪ (V (V C))) = (V (B C))
1914, 18eqtr3i 2375 . . 3 ((V B) ∪ C) = (V (B C))
2019ineq2i 3454 . 2 ((A C) ∩ ((V B) ∪ C)) = ((A C) ∩ (V (B C)))
21 invdif 3496 . 2 ((A C) ∩ (V (B C))) = ((A C) (B C))
2212, 20, 213eqtri 2377 1 ((A B) C) = ((A C) (B C))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1642  Vcvv 2859   cdif 3206  cun 3207  cin 3208  c0 3550
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-v 2861  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-ss 3259  df-nul 3551
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator