Theorem inundif 3752

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 3534	. . . 4 |- ( x e. ( A i^i B ) <-> ( x e. A /\ x e. B ) )
2		eldif 3333	. . . 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 951	. . 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 3493	1 |- ( ( A i^i B ) u. ( A \ B ) ) = A

Syntax hints:   -. wn 3   \/ wo 368   /\ wa 369   = wceq 1369   e. wcel 1756   \ cdif 3320   u. cun 3321   i^i cin 3322

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2969  df-dif 3326  df-un 3328  df-in 3330

This theorem is referenced by:  resasplit  5576  fresaun  5577  fresaunres2  5578  ixpfi2  7601  hashun3  12139  prmreclem2  13970  mvdco  15942  sylow2a  16109  ablfac1eu  16562  basdif0  18533  neitr  18759  cmpfi  18986  ptbasfi  19129  ptcnplem  19169  fin1aufil  19480  ismbl2  20985  volinun  21002  voliunlem2  21007  mbfeqalem  21095  itg2cnlem2  21215  dvres2lem  21360  imadifxp  25890  ofpreima2  25936  partfun  25944  resf1o  25981  measun  26577  measunl  26582  sibfof  26678  probdif  26755