Theorem inundif 4430

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 3919	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
2		eldif 3913	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
3	1, 2	orbi12i 914	. . 3 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∨ 𝑥 ∈ (𝐴 ∖ 𝐵)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∨ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)))
4		pm4.42 1053	. . 3 ⊢ (𝑥 ∈ 𝐴 ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∨ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)))
5	3, 4	bitr4i 278	. 2 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∨ 𝑥 ∈ (𝐴 ∖ 𝐵)) ↔ 𝑥 ∈ 𝐴)
6	5	uneqri 4107	1 ⊢ ((𝐴 ∩ 𝐵) ∪ (𝐴 ∖ 𝐵)) = 𝐴

Syntax hints:  ¬ wn 3   ∧ wa 395   ∨ wo 847   = wceq 1540   ∈ wcel 2109   ∖ cdif 3900   ∪ cun 3901   ∩ cin 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-dif 3906  df-un 3908  df-in 3910

This theorem is referenced by:  iunxdif3  5044  partfun  6629  resasplit  6694  fresaun  6695  fresaunres2  6696  ixpfi2  9240  hashun3  14291  prmreclem2  16829  mvdco  19324  sylow2a  19498  ablfac1eu  19954  basdif0  22838  neitr  23065  cmpfi  23293  ptbasfi  23466  ptcnplem  23506  fin1aufil  23817  ismbl2  25426  volinun  25445  voliunlem2  25450  mbfeqalem2  25541  itg2cnlem2  25661  dvres2lem  25809  indifundif  32468  imadifxp  32545  ofpreima2  32609  resf1o  32673  indsumin  32805  gsummptres  33005  tocyccntz  33086  measun  34178  measunl  34183  inelcarsg  34279  carsgclctun  34289  sibfof  34308  probdif  34388  hgt750lemd  34616  mthmpps  35555  clcnvlem  43596  radcnvrat  44287  sumnnodd  45611  ovolsplit  45969  omelesplit  46499  ovnsplit  46629