Theorem inundif 4304

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 4053	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
2		eldif 3835	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
3	1, 2	orbi12i 898	. . 3 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∨ 𝑥 ∈ (𝐴 ∖ 𝐵)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∨ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)))
4		pm4.42 1034	. . 3 ⊢ (𝑥 ∈ 𝐴 ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∨ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)))
5	3, 4	bitr4i 270	. 2 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∨ 𝑥 ∈ (𝐴 ∖ 𝐵)) ↔ 𝑥 ∈ 𝐴)
6	5	uneqri 4012	1 ⊢ ((𝐴 ∩ 𝐵) ∪ (𝐴 ∖ 𝐵)) = 𝐴

Syntax hints:  ¬ wn 3   ∧ wa 387   ∨ wo 833   = wceq 1507   ∈ wcel 2048   ∖ cdif 3822   ∪ cun 3823   ∩ cin 3824

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-v 3411  df-dif 3828  df-un 3830  df-in 3832

This theorem is referenced by:  iunxdif3  4877  resasplit  6371  fresaun  6372  fresaunres2  6373  ixpfi2  8609  hashun3  13551  prmreclem2  16099  mvdco  18324  sylow2a  18495  ablfac1eu  18935  basdif0  21255  neitr  21482  cmpfi  21710  ptbasfi  21883  ptcnplem  21923  fin1aufil  22234  ismbl2  23821  volinun  23840  voliunlem2  23845  mbfeqalem2  23936  itg2cnlem2  24056  dvres2lem  24201  indifundif  30049  imadifxp  30107  ofpreima2  30163  partfun  30173  resf1o  30207  gsummptres  30485  indsumin  30882  measun  31072  measunl  31077  inelcarsg  31171  carsgclctun  31181  sibfof  31200  probdif  31281  hgt750lemd  31528  mthmpps  32289  clcnvlem  39291  radcnvrat  40006  sumnnodd  41288  ovolsplit  41650  omelesplit  42177  ovnsplit  42307