Theorem inundif 4479

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

Syntax hints:  ¬ wn 3   ∧ wa 395   ∨ wo 848   = wceq 1540   ∈ wcel 2108   ∖ cdif 3948   ∪ cun 3949   ∩ cin 3950

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-dif 3954  df-un 3956  df-in 3958

This theorem is referenced by:  iunxdif3  5095  partfun  6715  resasplit  6778  fresaun  6779  fresaunres2  6780  ixpfi2  9390  hashun3  14423  prmreclem2  16955  mvdco  19463  sylow2a  19637  ablfac1eu  20093  basdif0  22960  neitr  23188  cmpfi  23416  ptbasfi  23589  ptcnplem  23629  fin1aufil  23940  ismbl2  25562  volinun  25581  voliunlem2  25586  mbfeqalem2  25677  itg2cnlem2  25797  dvres2lem  25945  indifundif  32543  imadifxp  32614  ofpreima2  32676  resf1o  32741  indsumin  32847  gsummptres  33055  tocyccntz  33164  measun  34212  measunl  34217  inelcarsg  34313  carsgclctun  34323  sibfof  34342  probdif  34422  hgt750lemd  34663  mthmpps  35587  clcnvlem  43636  radcnvrat  44333  sumnnodd  45645  ovolsplit  46003  omelesplit  46533  ovnsplit  46663