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

Theorem difundir 3732
Description: Distributive law for class difference. (Contributed by NM, 17-Aug-2004.)
Assertion
Ref Expression
difundir  |-  ( ( A  u.  B ) 
\  C )  =  ( ( A  \  C )  u.  ( B  \  C ) )

Proof of Theorem difundir
StepHypRef Expression
1 indir 3727 . 2  |-  ( ( A  u.  B )  i^i  ( _V  \  C ) )  =  ( ( A  i^i  ( _V  \  C ) )  u.  ( B  i^i  ( _V  \  C ) ) )
2 invdif 3720 . 2  |-  ( ( A  u.  B )  i^i  ( _V  \  C ) )  =  ( ( A  u.  B )  \  C
)
3 invdif 3720 . . 3  |-  ( A  i^i  ( _V  \  C ) )  =  ( A  \  C
)
4 invdif 3720 . . 3  |-  ( B  i^i  ( _V  \  C ) )  =  ( B  \  C
)
53, 4uneq12i 3624 . 2  |-  ( ( A  i^i  ( _V 
\  C ) )  u.  ( B  i^i  ( _V  \  C ) ) )  =  ( ( A  \  C
)  u.  ( B 
\  C ) )
61, 2, 53eqtr3i 2466 1  |-  ( ( A  u.  B ) 
\  C )  =  ( ( A  \  C )  u.  ( B  \  C ) )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437   _Vcvv 3087    \ cdif 3439    u. cun 3440    i^i cin 3441
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ral 2787  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449
This theorem is referenced by:  dfsymdif3  3744  symdif1OLD  3745  difun2  3881  diftpsn3  4141  strleun  15182  mreexmrid  15500  mreexexlem2d  15502  mvdco  17037  dprd2da  17610  dmdprdsplit2lem  17613  ablfac1eulem  17640  lbsextlem4  18319  opsrtoslem2  18643  nulmbl2  22367  uniioombllem3  22420  ex-dif  25718  indifundif  27988  imadifxp  28051  ballotlemfp1  29150  ballotlemgun  29183  onint1  30894  poimirlem2  31646  poimirlem6  31650  poimirlem7  31651  poimirlem8  31652  poimirlem22  31666  dvmptfprodlem  37388  fourierdlem102  37640  fourierdlem114  37652  caragenuncllem  37842  carageniuncllem1  37851
  Copyright terms: Public domain W3C validator