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

Theorem indif2 4017
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 3970 . 2 ((𝐴𝐵) ∩ (V ∖ 𝐶)) = (𝐴 ∩ (𝐵 ∩ (V ∖ 𝐶)))
2 invdif 4015 . 2 ((𝐴𝐵) ∩ (V ∖ 𝐶)) = ((𝐴𝐵) ∖ 𝐶)
3 invdif 4015 . . 3 (𝐵 ∩ (V ∖ 𝐶)) = (𝐵𝐶)
43ineq2i 3960 . 2 (𝐴 ∩ (𝐵 ∩ (V ∖ 𝐶))) = (𝐴 ∩ (𝐵𝐶))
51, 2, 43eqtr3ri 2801 1 (𝐴 ∩ (𝐵𝐶)) = ((𝐴𝐵) ∖ 𝐶)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1630  Vcvv 3349  cdif 3718  cin 3720
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ral 3065  df-rab 3069  df-v 3351  df-dif 3724  df-in 3728
This theorem is referenced by:  indif1  4018  indifcom  4019  wfi  5856  marypha1lem  8494  difopn  21058  restcld  21196  difmbl  23530  voliunlem1  23537  difuncomp  29701  imadifxp  29746  difelcarsg  30706  carsgclctunlem1  30713  frpoind  32071  frind  32074  topbnd  32650  bj-disj2r  33338  mblfinlem3  33774  mblfinlem4  33775  gneispace  38951  saldifcl2  41057  caragenuncllem  41240  carageniuncllem1  41249
  Copyright terms: Public domain W3C validator