Theorem inundif 4188

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 3947	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵))
2		eldif 3733	. . . 4 ⊢ (𝑥 ∈ (𝐴 ∖ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵))
3	1, 2	orbi12i 900	. . 3 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∨ 𝑥 ∈ (𝐴 ∖ 𝐵)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∨ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)))
4		pm4.42 1040	. . 3 ⊢ (𝑥 ∈ 𝐴 ↔ ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) ∨ (𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵)))
5	3, 4	bitr4i 267	. 2 ⊢ ((𝑥 ∈ (𝐴 ∩ 𝐵) ∨ 𝑥 ∈ (𝐴 ∖ 𝐵)) ↔ 𝑥 ∈ 𝐴)
6	5	uneqri 3906	1 ⊢ ((𝐴 ∩ 𝐵) ∪ (𝐴 ∖ 𝐵)) = 𝐴

Syntax hints:  ¬ wn 3   ∧ wa 382   ∨ wo 836   = wceq 1631   ∈ wcel 2145   ∖ cdif 3720   ∪ cun 3721   ∩ cin 3722

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-dif 3726  df-un 3728  df-in 3730

This theorem is referenced by:  iunxdif3  4740  resasplit  6212  fresaun  6213  fresaunres2  6214  ixpfi2  8418  hashun3  13368  prmreclem2  15821  mvdco  18065  sylow2a  18234  ablfac1eu  18673  basdif0  20971  neitr  21198  cmpfi  21425  ptbasfi  21598  ptcnplem  21638  fin1aufil  21949  ismbl2  23508  volinun  23527  voliunlem2  23532  mbfeqalem  23622  itg2cnlem2  23742  dvres2lem  23887  indifundif  29687  imadifxp  29745  ofpreima2  29799  partfun  29808  resf1o  29838  gsummptres  30117  indsumin  30417  measun  30607  measunl  30612  inelcarsg  30706  carsgclctun  30716  sibfof  30735  probdif  30815  hgt750lemd  31059  mthmpps  31810  clcnvlem  38449  radcnvrat  39032  sumnnodd  40373  ovolsplit  40715  omelesplit  41245  ovnsplit  41375