# Metamath Proof Explorer

## Theorem inundif

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)

Ref Expression
Assertion inundif ${⊢}\left({A}\cap {B}\right)\cup \left({A}\setminus {B}\right)={A}$

### Proof

Step Hyp Ref Expression
1 elin ${⊢}{x}\in \left({A}\cap {B}\right)↔\left({x}\in {A}\wedge {x}\in {B}\right)$
2 eldif ${⊢}{x}\in \left({A}\setminus {B}\right)↔\left({x}\in {A}\wedge ¬{x}\in {B}\right)$
3 1 2 orbi12i ${⊢}\left({x}\in \left({A}\cap {B}\right)\vee {x}\in \left({A}\setminus {B}\right)\right)↔\left(\left({x}\in {A}\wedge {x}\in {B}\right)\vee \left({x}\in {A}\wedge ¬{x}\in {B}\right)\right)$
4 pm4.42 ${⊢}{x}\in {A}↔\left(\left({x}\in {A}\wedge {x}\in {B}\right)\vee \left({x}\in {A}\wedge ¬{x}\in {B}\right)\right)$
5 3 4 bitr4i ${⊢}\left({x}\in \left({A}\cap {B}\right)\vee {x}\in \left({A}\setminus {B}\right)\right)↔{x}\in {A}$
6 5 uneqri ${⊢}\left({A}\cap {B}\right)\cup \left({A}\setminus {B}\right)={A}$