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

Step	Hyp	Ref	Expression
1		dfin2 3733	. 2
2		ddif 3635	. . 3
3	2	difeq2i 3618	. 2
4	1, 3	eqtri 2486	1

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