Theorem inundif 4412

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

Syntax hints:  ¬ wn 3   ∧ wa 396   ∨ wo 844   = wceq 1539   ∈ wcel 2106   ∖ cdif 3884   ∪ cun 3885   ∩ cin 3886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-dif 3890  df-un 3892  df-in 3894

This theorem is referenced by:  iunxdif3  5024  partfun  6580  resasplit  6644  fresaun  6645  fresaunres2  6646  ixpfi2  9117  hashun3  14099  prmreclem2  16618  mvdco  19053  sylow2a  19224  ablfac1eu  19676  basdif0  22103  neitr  22331  cmpfi  22559  ptbasfi  22732  ptcnplem  22772  fin1aufil  23083  ismbl2  24691  volinun  24710  voliunlem2  24715  mbfeqalem2  24806  itg2cnlem2  24927  dvres2lem  25074  indifundif  30873  imadifxp  30940  ofpreima2  31003  resf1o  31065  gsummptres  31312  tocyccntz  31411  indsumin  31990  measun  32179  measunl  32184  inelcarsg  32278  carsgclctun  32288  sibfof  32307  probdif  32387  hgt750lemd  32628  mthmpps  33544  clcnvlem  41231  radcnvrat  41932  sumnnodd  43171  ovolsplit  43529  omelesplit  44056  ovnsplit  44186