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

Theorem invdif 3738
 Description: Intersection with universal complement. Remark in [Stoll] p. 20. (Contributed by NM, 17-Aug-2004.)
Assertion
Ref Expression
invdif

Proof of Theorem invdif
StepHypRef Expression
1 dfin2 3733 . 2
2 ddif 3635 . . 3
32difeq2i 3618 . 2
41, 3eqtri 2486 1
 Colors of variables: wff setvar class Syntax hints:  =wceq 1395   cvv 3109  \cdif 3472  i^icin 3474 This theorem is referenced by:  indif2  3740  difundi  3749  difundir  3750  difindi  3751  difindir  3752  difdif2  3754  difun1  3757  undif1  3903  difdifdir  3915  frnsuppeq  6930  dfsup2  7922  dfsup2OLD  7923  nn0suppOLD  10875  fsets  14658  fsuppeq  31043 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rab 2816  df-v 3111  df-dif 3478  df-in 3482
 Copyright terms: Public domain W3C validator