Theorem inundif 4420

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 3906	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
2		eldif 3900	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
3	1, 2	orbi12i 915	. . 3 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∨ 𝑥 ∈ (𝐴 ∖ 𝐵)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∨ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)))
4		pm4.42 1054	. . 3 ⊢ (𝑥 ∈ 𝐴 ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∨ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)))
5	3, 4	bitr4i 278	. 2 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∨ 𝑥 ∈ (𝐴 ∖ 𝐵)) ↔ 𝑥 ∈ 𝐴)
6	5	uneqri 4097	1 ⊢ ((𝐴 ∩ 𝐵) ∪ (𝐴 ∖ 𝐵)) = 𝐴

Syntax hints:  ¬ wn 3   ∧ wa 395   ∨ wo 848   = wceq 1542   ∈ wcel 2114   ∖ cdif 3887   ∪ cun 3888   ∩ cin 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-dif 3893  df-un 3895  df-in 3897

This theorem is referenced by:  iunxdif3  5038  partfun  6640  resasplit  6705  fresaun  6706  fresaunres2  6707  ixpfi2  9254  hashun3  14340  prmreclem2  16882  mvdco  19414  sylow2a  19588  ablfac1eu  20044  basdif0  22931  neitr  23158  cmpfi  23386  ptbasfi  23559  ptcnplem  23599  fin1aufil  23910  ismbl2  25507  volinun  25526  voliunlem2  25531  mbfeqalem2  25622  itg2cnlem2  25742  dvres2lem  25890  indifundif  32612  imadifxp  32689  ofpreima2  32757  resf1o  32821  indsumin  32939  gsummptres  33131  tocyccntz  33223  measun  34374  measunl  34379  inelcarsg  34474  carsgclctun  34484  sibfof  34503  probdif  34583  hgt750lemd  34811  mthmpps  35783  clcnvlem  44071  radcnvrat  44762  sumnnodd  46081  ovolsplit  46437  omelesplit  46967  ovnsplit  47097