Theorem inundif 3906

Description: The intersection and class difference of a class with another class unite to give the original class. (Contributed by Paul Chapman, 5-Jun-2009.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)

Assertion

Ref	Expression
inundif

Proof of Theorem inundif

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elin 3686	. . . 4
2		eldif 3485	. . . 4
3	1, 2	orbi12i 521	. . 3
4		pm4.42 960	. . 3
5	3, 4	bitr4i 252	. 2
6	5	uneqri 3645	1

Syntax hints:  -.wn 3  \/wo 368  /\wa 369  =wceq 1395  e.wcel 1818  \cdif 3472  u.cun 3473  i^icin 3474

This theorem is referenced by:  resasplit  5760  fresaun  5761  fresaunres2  5762  ixpfi2  7838  hashun3  12452  prmreclem2  14435  mvdco  16470  sylow2a  16639  ablfac1eu  17124  basdif0  19454  neitr  19681  cmpfi  19908  ptbasfi  20082  ptcnplem  20122  fin1aufil  20433  ismbl2  21938  volinun  21956  voliunlem2  21961  mbfeqalem  22049  itg2cnlem2  22169  dvres2lem  22314  imadifxp  27458  ofpreima2  27508  partfun  27516  resf1o  27553  measun  28182  measunl  28187  sibfof  28282  probdif  28359  mthmpps  28942  radcnvrat  31195  sumnnodd  31636

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-or 370  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-v 3111  df-dif 3478  df-un 3480  df-in 3482