Theorem inundif 4477

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 3963	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
2		eldif 3957	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
3	1, 2	orbi12i 913	. . 3 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∨ 𝑥 ∈ (𝐴 ∖ 𝐵)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∨ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)))
4		pm4.42 1052	. . 3 ⊢ (𝑥 ∈ 𝐴 ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∨ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)))
5	3, 4	bitr4i 277	. 2 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∨ 𝑥 ∈ (𝐴 ∖ 𝐵)) ↔ 𝑥 ∈ 𝐴)
6	5	uneqri 4150	1 ⊢ ((𝐴 ∩ 𝐵) ∪ (𝐴 ∖ 𝐵)) = 𝐴

Syntax hints:  ¬ wn 3   ∧ wa 396   ∨ wo 845   = wceq 1541   ∈ wcel 2106   ∖ cdif 3944   ∪ cun 3945   ∩ cin 3946

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-dif 3950  df-un 3952  df-in 3954

This theorem is referenced by:  iunxdif3  5097  partfun  6694  resasplit  6758  fresaun  6759  fresaunres2  6760  ixpfi2  9346  hashun3  14340  prmreclem2  16846  mvdco  19307  sylow2a  19481  ablfac1eu  19937  basdif0  22447  neitr  22675  cmpfi  22903  ptbasfi  23076  ptcnplem  23116  fin1aufil  23427  ismbl2  25035  volinun  25054  voliunlem2  25059  mbfeqalem2  25150  itg2cnlem2  25271  dvres2lem  25418  indifundif  31749  imadifxp  31819  ofpreima2  31878  resf1o  31942  gsummptres  32191  tocyccntz  32290  indsumin  33008  measun  33197  measunl  33202  inelcarsg  33298  carsgclctun  33308  sibfof  33327  probdif  33407  hgt750lemd  33648  mthmpps  34561  clcnvlem  42359  radcnvrat  43058  sumnnodd  44332  ovolsplit  44690  omelesplit  45220  ovnsplit  45350