Theorem inundif 3879

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	|- ( ( A i^i B ) u. ( A \ B ) ) = A

Proof of Theorem inundif

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elin 3655	. . . 4 |- ( x e. ( A i^i B ) <-> ( x e. A /\ x e. B ) )
2		eldif 3452	. . . 4 |- ( x e. ( A \ B ) <-> ( x e. A /\ -. x e. B ) )
3	1, 2	orbi12i 523	. . 3 |- ( ( x e. ( A i^i B ) \/ x e. ( A \ B ) ) <-> ( ( x e. A /\ x e. B ) \/ ( x e. A /\ -. x e. B ) ) )
4		pm4.42 968	. . 3 |- ( x e. A <-> ( ( x e. A /\ x e. B ) \/ ( x e. A /\ -. x e. B ) ) )
5	3, 4	bitr4i 255	. 2 |- ( ( x e. ( A i^i B ) \/ x e. ( A \ B ) ) <-> x e. A )
6	5	uneqri 3614	1 |- ( ( A i^i B ) u. ( A \ B ) ) = A

Syntax hints:   -. wn 3   \/ wo 369   /\ wa 370   = wceq 1437   e. wcel 1870   \ cdif 3439   u. cun 3440   i^i cin 3441

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-v 3089  df-dif 3445  df-un 3447  df-in 3449

This theorem is referenced by:  resasplit  5770  fresaun  5771  fresaunres2  5772  ixpfi2  7878  hashun3  12560  prmreclem2  14824  mvdco  17037  sylow2a  17206  ablfac1eu  17641  basdif0  19899  neitr  20127  cmpfi  20354  ptbasfi  20527  ptcnplem  20567  fin1aufil  20878  ismbl2  22358  volinun  22376  voliunlem2  22381  mbfeqalem  22475  itg2cnlem2  22597  dvres2lem  22742  indifundif  27988  iunxdif3  28014  imadifxp  28051  ofpreima2  28109  partfun  28118  resf1o  28158  gsummptres  28386  measun  28872  measunl  28877  inelcarsg  28972  carsgclctun  28982  sibfof  29001  probdif  29079  mthmpps  30008  radcnvrat  36299  sumnnodd  37281  omelesplit  37847