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

Theorem indif2 4250
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 4199 . 2 ((𝐴𝐵) ∩ (V ∖ 𝐶)) = (𝐴 ∩ (𝐵 ∩ (V ∖ 𝐶)))
2 invdif 4248 . 2 ((𝐴𝐵) ∩ (V ∖ 𝐶)) = ((𝐴𝐵) ∖ 𝐶)
3 invdif 4248 . . 3 (𝐵 ∩ (V ∖ 𝐶)) = (𝐵𝐶)
43ineq2i 4189 . 2 (𝐴 ∩ (𝐵 ∩ (V ∖ 𝐶))) = (𝐴 ∩ (𝐵𝐶))
51, 2, 43eqtr3ri 2857 1 (𝐴 ∩ (𝐵𝐶)) = ((𝐴𝐵) ∖ 𝐶)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1530  Vcvv 3499  cdif 3936  cin 3938
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-rab 3151  df-v 3501  df-dif 3942  df-in 3946
This theorem is referenced by:  indif1  4251  indifcom  4252  wfi  6178  marypha1lem  8889  difopn  21560  restcld  21698  difmbl  24061  voliunlem1  24068  difuncomp  30221  imadifxp  30268  difelcarsg  31456  carsgclctunlem1  31463  frpoind  32966  frind  32971  topbnd  33558  bj-disj2r  34226  nlpineqsn  34560  mblfinlem3  34800  mblfinlem4  34801  rabdif  38974  gneispace  40351  saldifcl2  42479  caragenuncllem  42662  carageniuncllem1  42671
  Copyright terms: Public domain W3C validator