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

Theorem invdif 3688
Description: Intersection with universal complement. Remark in [Stoll] p. 20. (Contributed by NM, 17-Aug-2004.)
Assertion
Ref Expression
invdif  |-  ( A  i^i  ( _V  \  B ) )  =  ( A  \  B
)

Proof of Theorem invdif
StepHypRef Expression
1 dfin2 3683 . 2  |-  ( A  i^i  ( _V  \  B ) )  =  ( A  \  ( _V  \  ( _V  \  B ) ) )
2 ddif 3572 . . 3  |-  ( _V 
\  ( _V  \  B ) )  =  B
32difeq2i 3555 . 2  |-  ( A 
\  ( _V  \ 
( _V  \  B
) ) )  =  ( A  \  B
)
41, 3eqtri 2429 1  |-  ( A  i^i  ( _V  \  B ) )  =  ( A  \  B
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1403   _Vcvv 3056    \ cdif 3408    i^i cin 3410
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1637  ax-4 1650  ax-5 1723  ax-6 1769  ax-7 1812  ax-10 1859  ax-11 1864  ax-12 1876  ax-13 2024  ax-ext 2378
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1406  df-ex 1632  df-nf 1636  df-sb 1762  df-clab 2386  df-cleq 2392  df-clel 2395  df-nfc 2550  df-ral 2756  df-rab 2760  df-v 3058  df-dif 3414  df-in 3418
This theorem is referenced by:  indif2  3690  difundi  3699  difundir  3700  difindi  3701  difindir  3702  difdif2  3704  difun1  3707  undif1  3844  difdifdir  3856  frnsuppeq  6866  dfsup2  7854  dfsup2OLD  7855  nn0suppOLD  10809  fsets  14759  fsuppeq  35369
  Copyright terms: Public domain W3C validator