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

Theorem indif2 4071
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 4019 . 2 ((𝐴𝐵) ∩ (V ∖ 𝐶)) = (𝐴 ∩ (𝐵 ∩ (V ∖ 𝐶)))
2 invdif 4069 . 2 ((𝐴𝐵) ∩ (V ∖ 𝐶)) = ((𝐴𝐵) ∖ 𝐶)
3 invdif 4069 . . 3 (𝐵 ∩ (V ∖ 𝐶)) = (𝐵𝐶)
43ineq2i 4009 . 2 (𝐴 ∩ (𝐵 ∩ (V ∖ 𝐶))) = (𝐴 ∩ (𝐵𝐶))
51, 2, 43eqtr3ri 2830 1 (𝐴 ∩ (𝐵𝐶)) = ((𝐴𝐵) ∖ 𝐶)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1653  Vcvv 3385  cdif 3766  cin 3768
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2777
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-ral 3094  df-rab 3098  df-v 3387  df-dif 3772  df-in 3776
This theorem is referenced by:  indif1  4072  indifcom  4073  wfi  5931  marypha1lem  8581  difopn  21167  restcld  21305  difmbl  23651  voliunlem1  23658  difuncomp  29887  imadifxp  29931  difelcarsg  30888  carsgclctunlem1  30895  frpoind  32253  frind  32256  topbnd  32831  bj-disj2r  33505  mblfinlem3  33937  mblfinlem4  33938  gneispace  39210  saldifcl2  41285  caragenuncllem  41468  carageniuncllem1  41477
  Copyright terms: Public domain W3C validator