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

Theorem indif2 4176
 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 4125 . 2 ((𝐴𝐵) ∩ (V ∖ 𝐶)) = (𝐴 ∩ (𝐵 ∩ (V ∖ 𝐶)))
2 invdif 4174 . 2 ((𝐴𝐵) ∩ (V ∖ 𝐶)) = ((𝐴𝐵) ∖ 𝐶)
3 invdif 4174 . . 3 (𝐵 ∩ (V ∖ 𝐶)) = (𝐵𝐶)
43ineq2i 4115 . 2 (𝐴 ∩ (𝐵 ∩ (V ∖ 𝐶))) = (𝐴 ∩ (𝐵𝐶))
51, 2, 43eqtr3ri 2791 1 (𝐴 ∩ (𝐵𝐶)) = ((𝐴𝐵) ∖ 𝐶)
 Colors of variables: wff setvar class Syntax hints:   = wceq 1539  Vcvv 3410   ∖ cdif 3856   ∩ cin 3858 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 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-ext 2730 This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1542  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-rab 3080  df-v 3412  df-dif 3862  df-in 3866 This theorem is referenced by:  indif1  4177  indifcom  4178  wfi  6160  marypha1lem  8923  difopn  21727  restcld  21865  difmbl  24236  voliunlem1  24243  difuncomp  30408  imadifxp  30455  difelcarsg  31789  carsgclctunlem1  31796  frpoind  33320  frind  33328  topbnd  34055  bj-disj2r  34738  nlpineqsn  35098  mblfinlem3  35369  mblfinlem4  35370  rabdif  39691  gneispace  41203  saldifcl2  43327  caragenuncllem  43510  carageniuncllem1  43519
 Copyright terms: Public domain W3C validator