Theorem inundif 4445

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

Syntax hints:  ¬ wn 3   ∧ wa 395   ∨ wo 847   = wceq 1540   ∈ wcel 2109   ∖ cdif 3914   ∪ cun 3915   ∩ cin 3916

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-dif 3920  df-un 3922  df-in 3924

This theorem is referenced by:  iunxdif3  5062  partfun  6668  resasplit  6733  fresaun  6734  fresaunres2  6735  ixpfi2  9308  hashun3  14356  prmreclem2  16895  mvdco  19382  sylow2a  19556  ablfac1eu  20012  basdif0  22847  neitr  23074  cmpfi  23302  ptbasfi  23475  ptcnplem  23515  fin1aufil  23826  ismbl2  25435  volinun  25454  voliunlem2  25459  mbfeqalem2  25550  itg2cnlem2  25670  dvres2lem  25818  indifundif  32460  imadifxp  32537  ofpreima2  32597  resf1o  32660  indsumin  32792  gsummptres  32999  tocyccntz  33108  measun  34208  measunl  34213  inelcarsg  34309  carsgclctun  34319  sibfof  34338  probdif  34418  hgt750lemd  34646  mthmpps  35576  clcnvlem  43619  radcnvrat  44310  sumnnodd  45635  ovolsplit  45993  omelesplit  46523  ovnsplit  46653