MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  indifdir Structured version   Visualization version   Unicode version
Theorem indifdir 3883
Description: Distribute intersection over difference. (Contributed by Scott Fenton, 14-Apr-2011.)
Assertion
Ref Expression
indifdir |- ( ( A \ B ) i^i C ) = ( ( A i^i C ) \ ( B i^i C ) )
Proof of Theorem indifdir
Dummy variable x is distinct from all other variables.
StepHypRef Expression
1 pm3.24 926 . . . . . . . 8 |- -. ( x e. C /\ -. x e. C )
21intnan 960 . . . . . . 7 |- -. ( x e. A /\ ( x e. C /\ -. x e. C ) )
3 anass 681 . . . . . . 7 |- ( ( ( x e. A /\ x e. C ) /\ -. x e. C ) <-> ( x e. A /\ ( x e. C /\ -. x e. C ) ) )
42, 3mtbir 313 . . . . . 6 |- -. ( ( x e. A /\ x e. C ) /\ -. x e. C )
54biorfi 422 . . . . 5 |- ( ( ( x e. A /\ x e. C ) /\ -. x e. B ) <-> ( ( ( x e. A /\ x e. C ) /\ -. x e. B ) \/ ( ( x e. A /\ x e. C ) /\ -. x e. C ) ) )
6 an32 839 . . . . 5 |- ( ( ( x e. A /\ -. x e. B ) /\ x e. C ) <-> ( ( x e. A /\ x e. C ) /\ -. x e. B ) )
7 andi 911 . . . . 5 |- ( ( ( x e. A /\ x e. C ) /\ ( -. x e. B \/ -. x e. C ) ) <-> ( ( ( x e. A /\ x e. C ) /\ -. x e. B ) \/ ( ( x e. A /\ x e. C ) /\ -. x e. C ) ) )
85, 6, 73bitr4i 292 . . . 4 |- ( ( ( x e. A /\ -. x e. B ) /\ x e. C ) <-> ( ( x e. A /\ x e. C ) /\ ( -. x e. B \/ -. x e. C ) ) )
9 ianor 509 . . . . 5 |- ( -. ( x e. B /\ x e. C ) <-> ( -. x e. B \/ -. x e. C ) )
109anbi2i 730 . . . 4 |- ( ( ( x e. A /\ x e. C ) /\ -. ( x e. B /\ x e. C ) ) <-> ( ( x e. A /\ x e. C ) /\ ( -. x e. B \/ -. x e. C ) ) )
118, 10bitr4i 267 . . 3 |- ( ( ( x e. A /\ -. x e. B ) /\ x e. C ) <-> ( ( x e. A /\ x e. C ) /\ -. ( x e. B /\ x e. C ) ) )
12 elin 3796 . . . 4 |- ( x e. ( ( A \ B ) i^i C ) <-> ( x e. ( A \ B ) /\ x e. C ) )
13 eldif 3584 . . . . 5 |- ( x e. ( A \ B ) <-> ( x e. A /\ -. x e. B ) )
1413anbi1i 731 . . . 4 |- ( ( x e. ( A \ B ) /\ x e. C ) <-> ( ( x e. A /\ -. x e. B ) /\ x e. C ) )
1512, 14bitri 264 . . 3 |- ( x e. ( ( A \ B ) i^i C ) <-> ( ( x e. A /\ -. x e. B ) /\ x e. C ) )
16 eldif 3584 . . . 4 |- ( x e. ( ( A i^i C ) \ ( B i^i C ) ) <-> ( x e. ( A i^i C ) /\ -. x e. ( B i^i C ) ) )
17 elin 3796 . . . . 5 |- ( x e. ( A i^i C ) <-> ( x e. A /\ x e. C ) )
18 elin 3796 . . . . . 6 |- ( x e. ( B i^i C ) <-> ( x e. B /\ x e. C ) )
1918notbii 310 . . . . 5 |- ( -. x e. ( B i^i C ) <-> -. ( x e. B /\ x e. C ) )
2017, 19anbi12i 733 . . . 4 |- ( ( x e. ( A i^i C ) /\ -. x e. ( B i^i C ) ) <-> ( ( x e. A /\ x e. C ) /\ -. ( x e. B /\ x e. C ) ) )
2116, 20bitri 264 . . 3 |- ( x e. ( ( A i^i C ) \ ( B i^i C ) ) <-> ( ( x e. A /\ x e. C ) /\ -. ( x e. B /\ x e. C ) ) )
2211, 15, 213bitr4i 292 . 2 |- ( x e. ( ( A \ B ) i^i C ) <-> x e. ( ( A i^i C ) \ ( B i^i C ) ) )
2322eqriv 2619 1 |- ( ( A \ B ) i^i C ) = ( ( A i^i C ) \ ( B i^i C ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3   \/ wo 383   /\ wa 384   = wceq 1483   e. wcel 1990   \ cdif 3571   i^i cin 3573
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-dif 3577  df-in 3581
This theorem is referenced by:  preddif  5705  fresaun  6075  uniioombllem4  23354  subsalsal  40577
  Copyright terms: Public domain W3C validator