# Metamath Proof Explorer

## Theorem resundi

Description: Distributive law for restriction over union. Theorem 31 of Suppes p. 65. (Contributed by NM, 30-Sep-2002)

Ref Expression
Assertion resundi ${⊢}{{A}↾}_{\left({B}\cup {C}\right)}=\left({{A}↾}_{{B}}\right)\cup \left({{A}↾}_{{C}}\right)$

### Proof

Step Hyp Ref Expression
1 xpundir ${⊢}\left({B}\cup {C}\right)×\mathrm{V}=\left({B}×\mathrm{V}\right)\cup \left({C}×\mathrm{V}\right)$
2 1 ineq2i ${⊢}{A}\cap \left(\left({B}\cup {C}\right)×\mathrm{V}\right)={A}\cap \left(\left({B}×\mathrm{V}\right)\cup \left({C}×\mathrm{V}\right)\right)$
3 indi ${⊢}{A}\cap \left(\left({B}×\mathrm{V}\right)\cup \left({C}×\mathrm{V}\right)\right)=\left({A}\cap \left({B}×\mathrm{V}\right)\right)\cup \left({A}\cap \left({C}×\mathrm{V}\right)\right)$
4 2 3 eqtri ${⊢}{A}\cap \left(\left({B}\cup {C}\right)×\mathrm{V}\right)=\left({A}\cap \left({B}×\mathrm{V}\right)\right)\cup \left({A}\cap \left({C}×\mathrm{V}\right)\right)$
5 df-res ${⊢}{{A}↾}_{\left({B}\cup {C}\right)}={A}\cap \left(\left({B}\cup {C}\right)×\mathrm{V}\right)$
6 df-res ${⊢}{{A}↾}_{{B}}={A}\cap \left({B}×\mathrm{V}\right)$
7 df-res ${⊢}{{A}↾}_{{C}}={A}\cap \left({C}×\mathrm{V}\right)$
8 6 7 uneq12i ${⊢}\left({{A}↾}_{{B}}\right)\cup \left({{A}↾}_{{C}}\right)=\left({A}\cap \left({B}×\mathrm{V}\right)\right)\cup \left({A}\cap \left({C}×\mathrm{V}\right)\right)$
9 4 5 8 3eqtr4i ${⊢}{{A}↾}_{\left({B}\cup {C}\right)}=\left({{A}↾}_{{B}}\right)\cup \left({{A}↾}_{{C}}\right)$