MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  indif2 Structured version   Visualization version   GIF version

Theorem indif2 4281
Description: Bring an intersection in and out of a class difference. (Contributed by Jeff Hankins, 15-Jul-2009.)
Assertion
Ref Expression
indif2 (𝐴 ∩ (𝐵𝐶)) = ((𝐴𝐵) ∖ 𝐶)

Proof of Theorem indif2
StepHypRef Expression
1 inass 4228 . 2 ((𝐴𝐵) ∩ (V ∖ 𝐶)) = (𝐴 ∩ (𝐵 ∩ (V ∖ 𝐶)))
2 invdif 4279 . 2 ((𝐴𝐵) ∩ (V ∖ 𝐶)) = ((𝐴𝐵) ∖ 𝐶)
3 invdif 4279 . . 3 (𝐵 ∩ (V ∖ 𝐶)) = (𝐵𝐶)
43ineq2i 4217 . 2 (𝐴 ∩ (𝐵 ∩ (V ∖ 𝐶))) = (𝐴 ∩ (𝐵𝐶))
51, 2, 43eqtr3ri 2774 1 (𝐴 ∩ (𝐵𝐶)) = ((𝐴𝐵) ∖ 𝐶)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1540  Vcvv 3480  cdif 3948  cin 3950
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 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-in 3958
This theorem is referenced by:  indif1  4282  indifcom  4283  rabdif  4321  frpoind  6363  wfiOLD  6372  marypha1lem  9473  frind  9790  difopn  23042  restcld  23180  difmbl  25578  voliunlem1  25585  difuncomp  32566  imadifxp  32614  difelcarsg  34312  carsgclctunlem1  34319  topbnd  36325  bj-disj2r  37029  nlpineqsn  37409  mblfinlem3  37666  mblfinlem4  37667  gneispace  44147  saldifcl2  46343  caragenuncllem  46527  carageniuncllem1  46536  iscnrm3rlem1  48837
  Copyright terms: Public domain W3C validator