Theorem inundif 3905

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 3687	. . . 4 |- ( x e. ( A i^i B ) <-> ( x e. A /\ x e. B ) )
2		eldif 3486	. . . 4 |- ( x e. ( A \ B ) <-> ( x e. A /\ -. x e. B ) )
3	1, 2	orbi12i 521	. . 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 958	. . 3 |- ( x e. A <-> ( ( x e. A /\ x e. B ) \/ ( x e. A /\ -. x e. B ) ) )
5	3, 4	bitr4i 252	. 2 |- ( ( x e. ( A i^i B ) \/ x e. ( A \ B ) ) <-> x e. A )
6	5	uneqri 3646	1 |- ( ( A i^i B ) u. ( A \ B ) ) = A

Syntax hints:   -. wn 3   \/ wo 368   /\ wa 369   = wceq 1379   e. wcel 1767   \ cdif 3473   u. cun 3474   i^i cin 3475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-dif 3479  df-un 3481  df-in 3483

This theorem is referenced by:  resasplit  5754  fresaun  5755  fresaunres2  5756  ixpfi2  7817  hashun3  12419  prmreclem2  14293  mvdco  16273  sylow2a  16442  ablfac1eu  16923  basdif0  19237  neitr  19463  cmpfi  19690  ptbasfi  19833  ptcnplem  19873  fin1aufil  20184  ismbl2  21689  volinun  21707  voliunlem2  21712  mbfeqalem  21800  itg2cnlem2  21920  dvres2lem  22065  imadifxp  27147  ofpreima2  27196  partfun  27204  resf1o  27241  measun  27838  measunl  27843  sibfof  27938  probdif  28015  sumnnodd  31188