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

Theorem invdif 3724
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 3719 . 2  |-  ( A  i^i  ( _V  \  B ) )  =  ( A  \  ( _V  \  ( _V  \  B ) ) )
2 ddif 3621 . . 3  |-  ( _V 
\  ( _V  \  B ) )  =  B
32difeq2i 3604 . 2  |-  ( A 
\  ( _V  \ 
( _V  \  B
) ) )  =  ( A  \  B
)
41, 3eqtri 2472 1  |-  ( A  i^i  ( _V  \  B ) )  =  ( A  \  B
)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1383   _Vcvv 3095    \ 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 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ral 2798  df-rab 2802  df-v 3097  df-dif 3464  df-in 3468
This theorem is referenced by:  indif2  3726  difundi  3735  difundir  3736  difindi  3737  difindir  3738  difdif2  3740  difun1  3743  undif1  3889  difdifdir  3901  frnsuppeq  6915  dfsup2  7904  dfsup2OLD  7905  nn0suppOLD  10857  fsets  14639  fsuppeq  31018
  Copyright terms: Public domain W3C validator