# Metamath Proof Explorer

## Theorem difundir

Description: Distributive law for class difference. (Contributed by NM, 17-Aug-2004)

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

### Proof

Step Hyp Ref Expression
1 indir ${⊢}\left({A}\cup {B}\right)\cap \left(\mathrm{V}\setminus {C}\right)=\left({A}\cap \left(\mathrm{V}\setminus {C}\right)\right)\cup \left({B}\cap \left(\mathrm{V}\setminus {C}\right)\right)$
2 invdif ${⊢}\left({A}\cup {B}\right)\cap \left(\mathrm{V}\setminus {C}\right)=\left({A}\cup {B}\right)\setminus {C}$
3 invdif ${⊢}{A}\cap \left(\mathrm{V}\setminus {C}\right)={A}\setminus {C}$
4 invdif ${⊢}{B}\cap \left(\mathrm{V}\setminus {C}\right)={B}\setminus {C}$
5 3 4 uneq12i ${⊢}\left({A}\cap \left(\mathrm{V}\setminus {C}\right)\right)\cup \left({B}\cap \left(\mathrm{V}\setminus {C}\right)\right)=\left({A}\setminus {C}\right)\cup \left({B}\setminus {C}\right)$
6 1 2 5 3eqtr3i ${⊢}\left({A}\cup {B}\right)\setminus {C}=\left({A}\setminus {C}\right)\cup \left({B}\setminus {C}\right)$