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

Theorem indif2 3738
Description: Bring an intersection in and out of a class difference. (Contributed by Jeff Hankins, 15-Jul-2009.)
Assertion
Ref Expression
indif2  |-  ( A  i^i  ( B  \  C ) )  =  ( ( A  i^i  B )  \  C )

Proof of Theorem indif2
StepHypRef Expression
1 inass 3694 . 2  |-  ( ( A  i^i  B )  i^i  ( _V  \  C ) )  =  ( A  i^i  ( B  i^i  ( _V  \  C ) ) )
2 invdif 3736 . 2  |-  ( ( A  i^i  B )  i^i  ( _V  \  C ) )  =  ( ( A  i^i  B )  \  C )
3 invdif 3736 . . 3  |-  ( B  i^i  ( _V  \  C ) )  =  ( B  \  C
)
43ineq2i 3683 . 2  |-  ( A  i^i  ( B  i^i  ( _V  \  C ) ) )  =  ( A  i^i  ( B 
\  C ) )
51, 2, 43eqtr3ri 2492 1  |-  ( A  i^i  ( B  \  C ) )  =  ( ( A  i^i  B )  \  C )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1398   _Vcvv 3106    \ cdif 3458    i^i cin 3460
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2809  df-rab 2813  df-v 3108  df-dif 3464  df-in 3468
This theorem is referenced by:  indif1  3739  indifcom  3740  marypha1lem  7885  difopn  19702  restcld  19840  difmbl  22119  voliunlem1  22126  imadifxp  27672  difelcarsg  28518  carsgclctunlem1  28525  wfi  29527  frind  29563  mblfinlem3  30293  mblfinlem4  30294  topbnd  30382
  Copyright terms: Public domain W3C validator