Theorem inundif 4480

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 3960	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
2		eldif 3954	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
3	1, 2	orbi12i 912	. . 3 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∨ 𝑥 ∈ (𝐴 ∖ 𝐵)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∨ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)))
4		pm4.42 1051	. . 3 ⊢ (𝑥 ∈ 𝐴 ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∨ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)))
5	3, 4	bitr4i 277	. 2 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∨ 𝑥 ∈ (𝐴 ∖ 𝐵)) ↔ 𝑥 ∈ 𝐴)
6	5	uneqri 4148	1 ⊢ ((𝐴 ∩ 𝐵) ∪ (𝐴 ∖ 𝐵)) = 𝐴

Syntax hints:  ¬ wn 3   ∧ wa 394   ∨ wo 845   = wceq 1533   ∈ wcel 2098   ∖ cdif 3941   ∪ cun 3942   ∩ cin 3943

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-v 3463  df-dif 3947  df-un 3949  df-in 3951

This theorem is referenced by:  iunxdif3  5099  partfun  6703  resasplit  6767  fresaun  6768  fresaunres2  6769  ixpfi2  9376  hashun3  14379  prmreclem2  16889  mvdco  19412  sylow2a  19586  ablfac1eu  20042  basdif0  22900  neitr  23128  cmpfi  23356  ptbasfi  23529  ptcnplem  23569  fin1aufil  23880  ismbl2  25500  volinun  25519  voliunlem2  25524  mbfeqalem2  25615  itg2cnlem2  25736  dvres2lem  25883  indifundif  32400  imadifxp  32470  ofpreima2  32533  resf1o  32594  gsummptres  32856  tocyccntz  32957  indsumin  33772  measun  33961  measunl  33966  inelcarsg  34062  carsgclctun  34072  sibfof  34091  probdif  34171  hgt750lemd  34411  mthmpps  35323  clcnvlem  43195  radcnvrat  43893  sumnnodd  45156  ovolsplit  45514  omelesplit  46044  ovnsplit  46174