Theorem resundi 5860

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

Assertion

Ref	Expression
resundi	⊢ (𝐴 ↾ (𝐵 ∪ 𝐶)) = ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶))

Proof of Theorem resundi

Step	Hyp	Ref	Expression
1		xpundir 5614	. . . 4 ⊢ ((𝐵 ∪ 𝐶) × V) = ((𝐵 × V) ∪ (𝐶 × V))
2	1	ineq2i 4184	. . 3 ⊢ (𝐴 ∩ ((𝐵 ∪ 𝐶) × V)) = (𝐴 ∩ ((𝐵 × V) ∪ (𝐶 × V)))
3		indi 4248	. . 3 ⊢ (𝐴 ∩ ((𝐵 × V) ∪ (𝐶 × V))) = ((𝐴 ∩ (𝐵 × V)) ∪ (𝐴 ∩ (𝐶 × V)))
4	2, 3	eqtri 2842	. 2 ⊢ (𝐴 ∩ ((𝐵 ∪ 𝐶) × V)) = ((𝐴 ∩ (𝐵 × V)) ∪ (𝐴 ∩ (𝐶 × V)))
5		df-res 5560	. 2 ⊢ (𝐴 ↾ (𝐵 ∪ 𝐶)) = (𝐴 ∩ ((𝐵 ∪ 𝐶) × V))
6		df-res 5560	. . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
7		df-res 5560	. . 3 ⊢ (𝐴 ↾ 𝐶) = (𝐴 ∩ (𝐶 × V))
8	6, 7	uneq12i 4135	. 2 ⊢ ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶)) = ((𝐴 ∩ (𝐵 × V)) ∪ (𝐴 ∩ (𝐶 × V)))
9	4, 5, 8	3eqtr4i 2852	1 ⊢ (𝐴 ↾ (𝐵 ∪ 𝐶)) = ((𝐴 ↾ 𝐵) ∪ (𝐴 ↾ 𝐶))

Syntax hints:   = wceq 1531  Vcvv 3493   ∪ cun 3932   ∩ cin 3933   × cxp 5546   ↾ cres 5550

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-rab 3145  df-v 3495  df-un 3939  df-in 3941  df-opab 5120  df-xp 5554  df-res 5560

This theorem is referenced by:  imaundi  6001  relresfld  6120  resasplit  6541  fresaunres2  6543  residpr  6898  fnsnsplit  6939  tfrlem16  8021  mapunen  8678  fnfi  8788  fseq1p1m1  12973  resunimafz0  13795  gsum2dlem2  19083  dprd2da  19156  evlseu  20288  ptuncnv  22407  mbfres2  24238  reldisjun  30345  ffsrn  30457  resf1o  30458  symgcom  30720  tocyc01  30753  cvmliftlem10  32534  eqfunresadj  32997  nosupbnd2lem1  33208  poimirlem9  34893  eldioph4b  39398  pwssplit4  39679  undmrnresiss  39954  relexp0a  40051  rnresun  41425