Theorem inundif 4429

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

Syntax hints:  ¬ wn 3   ∧ wa 395   ∨ wo 847   = wceq 1541   ∈ wcel 2113   ∖ cdif 3896   ∪ cun 3897   ∩ cin 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-dif 3902  df-un 3904  df-in 3906

This theorem is referenced by:  iunxdif3  5048  partfun  6637  resasplit  6702  fresaun  6703  fresaunres2  6704  ixpfi2  9248  hashun3  14305  prmreclem2  16843  mvdco  19372  sylow2a  19546  ablfac1eu  20002  basdif0  22895  neitr  23122  cmpfi  23350  ptbasfi  23523  ptcnplem  23563  fin1aufil  23874  ismbl2  25482  volinun  25501  voliunlem2  25506  mbfeqalem2  25597  itg2cnlem2  25717  dvres2lem  25865  indifundif  32548  imadifxp  32625  ofpreima2  32693  resf1o  32758  indsumin  32892  gsummptres  33084  tocyccntz  33175  measun  34317  measunl  34322  inelcarsg  34417  carsgclctun  34427  sibfof  34446  probdif  34526  hgt750lemd  34754  mthmpps  35725  clcnvlem  43806  radcnvrat  44497  sumnnodd  45818  ovolsplit  46174  omelesplit  46704  ovnsplit  46834