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

Theorem invdif 3732
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 3727 . 2  |-  ( A  i^i  ( _V  \  B ) )  =  ( A  \  ( _V  \  ( _V  \  B ) ) )
2 ddif 3629 . . 3  |-  ( _V 
\  ( _V  \  B ) )  =  B
32difeq2i 3612 . 2  |-  ( A 
\  ( _V  \ 
( _V  \  B
) ) )  =  ( A  \  B
)
41, 3eqtri 2489 1  |-  ( A  i^i  ( _V  \  B ) )  =  ( A  \  B
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1374   _Vcvv 3106    \ cdif 3466    i^i cin 3468
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ral 2812  df-rab 2816  df-v 3108  df-dif 3472  df-in 3476
This theorem is referenced by:  indif2  3734  difundi  3743  difundir  3744  difindi  3745  difindir  3746  difdif2  3748  difun1  3751  undif1  3895  difdifdir  3907  frnsuppeq  6903  dfsup2  7891  dfsup2OLD  7892  nn0suppOLD  10839  fsets  14505  fsuppeq  30636
  Copyright terms: Public domain W3C validator