Theorem inundif 4379

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

Syntax hints:  ¬ wn 3   ∧ wa 399   ∨ wo 847   = wceq 1543   ∈ wcel 2112   ∖ cdif 3850   ∪ cun 3851   ∩ cin 3852

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-dif 3856  df-un 3858  df-in 3860

This theorem is referenced by:  iunxdif3  4989  partfun  6503  resasplit  6567  fresaun  6568  fresaunres2  6569  ixpfi2  8952  hashun3  13916  prmreclem2  16433  mvdco  18791  sylow2a  18962  ablfac1eu  19414  basdif0  21804  neitr  22031  cmpfi  22259  ptbasfi  22432  ptcnplem  22472  fin1aufil  22783  ismbl2  24378  volinun  24397  voliunlem2  24402  mbfeqalem2  24493  itg2cnlem2  24614  dvres2lem  24761  indifundif  30546  imadifxp  30613  ofpreima2  30677  resf1o  30739  gsummptres  30985  tocyccntz  31084  indsumin  31656  measun  31845  measunl  31850  inelcarsg  31944  carsgclctun  31954  sibfof  31973  probdif  32053  hgt750lemd  32294  mthmpps  33211  clcnvlem  40848  radcnvrat  41546  sumnnodd  42789  ovolsplit  43147  omelesplit  43674  ovnsplit  43804