Theorem inundif 3856

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 3628	. . . 4 |- ( x e. ( A i^i B ) <-> ( x e. A /\ x e. B ) )
2		eldif 3425	. . . 4 |- ( x e. ( A \ B ) <-> ( x e. A /\ -. x e. B ) )
3	1, 2	orbi12i 528	. . 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 977	. . 3 |- ( x e. A <-> ( ( x e. A /\ x e. B ) \/ ( x e. A /\ -. x e. B ) ) )
5	3, 4	bitr4i 260	. 2 |- ( ( x e. ( A i^i B ) \/ x e. ( A \ B ) ) <-> x e. A )
6	5	uneqri 3587	1 |- ( ( A i^i B ) u. ( A \ B ) ) = A

Syntax hints:   -. wn 3   \/ wo 374   /\ wa 375   = wceq 1454   e. wcel 1897   \ cdif 3412   u. cun 3413   i^i cin 3414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-v 3058  df-dif 3418  df-un 3420  df-in 3422

This theorem is referenced by:  resasplit  5775  fresaun  5776  fresaunres2  5777  ixpfi2  7897  hashun3  12594  prmreclem2  14909  mvdco  17134  sylow2a  17319  ablfac1eu  17754  basdif0  20016  neitr  20244  cmpfi  20471  ptbasfi  20644  ptcnplem  20684  fin1aufil  20995  ismbl2  22529  volinun  22547  voliunlem2  22552  mbfeqalem  22646  itg2cnlem2  22768  dvres2lem  22913  indifundif  28200  iunxdif3  28223  imadifxp  28260  ofpreima2  28317  partfun  28326  resf1o  28363  gsummptres  28595  measun  29081  measunl  29086  inelcarsg  29191  carsgclctun  29201  sibfof  29221  probdif  29301  mthmpps  30268  clcnvlem  36274  radcnvrat  36706  sumnnodd  37747  omelesplit  38376