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

Theorem difundir 3748
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 3743 . 2  |-  ( ( A  u.  B )  i^i  ( _V  \  C ) )  =  ( ( A  i^i  ( _V  \  C ) )  u.  ( B  i^i  ( _V  \  C ) ) )
2 invdif 3736 . 2  |-  ( ( A  u.  B )  i^i  ( _V  \  C ) )  =  ( ( A  u.  B )  \  C
)
3 invdif 3736 . . 3  |-  ( A  i^i  ( _V  \  C ) )  =  ( A  \  C
)
4 invdif 3736 . . 3  |-  ( B  i^i  ( _V  \  C ) )  =  ( B  \  C
)
53, 4uneq12i 3642 . 2  |-  ( ( A  i^i  ( _V 
\  C ) )  u.  ( B  i^i  ( _V  \  C ) ) )  =  ( ( A  \  C
)  u.  ( B 
\  C ) )
61, 2, 53eqtr3i 2491 1  |-  ( ( A  u.  B ) 
\  C )  =  ( ( A  \  C )  u.  ( B  \  C ) )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1398   _Vcvv 3106    \ cdif 3458    u. cun 3459    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-or 368  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-un 3466  df-in 3468
This theorem is referenced by:  dfsymdif3  3760  symdif1OLD  3761  difun2  3895  diftpsn3  4154  strleun  14814  mreexmrid  15132  mreexexlem2d  15134  mvdco  16669  dprd2da  17286  dmdprdsplit2lem  17289  ablfac1eulem  17318  lbsextlem4  18002  opsrtoslem2  18344  nulmbl2  22113  uniioombllem3  22160  ex-dif  25346  indifundif  27616  imadifxp  27672  ballotlemfp1  28694  ballotlemgun  28727  onint1  30142  dvmptfprodlem  31980  fourierdlem102  32230  fourierdlem114  32242
  Copyright terms: Public domain W3C validator