Theorem resres 5951

Description: The restriction of a restriction. (Contributed by NM, 27-Mar-2008.)

Assertion

Ref	Expression
resres	⊢ ((𝐴 ↾ 𝐵) ↾ 𝐶) = (𝐴 ↾ (𝐵 ∩ 𝐶))

Proof of Theorem resres

Step	Hyp	Ref	Expression
1		df-res 5636	. 2 ⊢ ((𝐴 ↾ 𝐵) ↾ 𝐶) = ((𝐴 ↾ 𝐵) ∩ (𝐶 × V))
2		df-res 5636	. . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
3	2	ineq1i 4157	. 2 ⊢ ((𝐴 ↾ 𝐵) ∩ (𝐶 × V)) = ((𝐴 ∩ (𝐵 × V)) ∩ (𝐶 × V))
4		xpindir 5783	. . . 4 ⊢ ((𝐵 ∩ 𝐶) × V) = ((𝐵 × V) ∩ (𝐶 × V))
5	4	ineq2i 4158	. . 3 ⊢ (𝐴 ∩ ((𝐵 ∩ 𝐶) × V)) = (𝐴 ∩ ((𝐵 × V) ∩ (𝐶 × V)))
6		df-res 5636	. . 3 ⊢ (𝐴 ↾ (𝐵 ∩ 𝐶)) = (𝐴 ∩ ((𝐵 ∩ 𝐶) × V))
7		inass 4169	. . 3 ⊢ ((𝐴 ∩ (𝐵 × V)) ∩ (𝐶 × V)) = (𝐴 ∩ ((𝐵 × V) ∩ (𝐶 × V)))
8	5, 6, 7	3eqtr4ri 2771	. 2 ⊢ ((𝐴 ∩ (𝐵 × V)) ∩ (𝐶 × V)) = (𝐴 ↾ (𝐵 ∩ 𝐶))
9	1, 3, 8	3eqtri 2764	1 ⊢ ((𝐴 ↾ 𝐵) ↾ 𝐶) = (𝐴 ↾ (𝐵 ∩ 𝐶))

Syntax hints:   = wceq 1542  Vcvv 3430   ∩ cin 3889   × cxp 5622   ↾ cres 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-opab 5149  df-xp 5630  df-rel 5631  df-res 5636

This theorem is referenced by:  rescom  5961  resabs1  5965  resima2  5975  resmpt3  5997  resdisj  6127  rescnvcnv  6162  fresin  6703  resdif  6795  curry1  8047  curry2  8050  frrlem4  8232  pmresg  8811  gruima  10716  rlimres  15511  lo1res  15512  rlimresb  15518  lo1eq  15521  rlimeq  15522  fsets  17130  setsid  17168  sscres  17781  gsumzres  19875  txkgen  23627  tsmsres  24119  ressxms  24500  ressms  24501  dvres  25888  dvres3a  25891  cpnres  25914  dvmptres3  25933  rlimcnp2  26943  df1stres  32792  df2ndres  32793  indf1ofs  32941  dfrcl2  44119  relexpaddss  44163  limsupresuz  46149  liminfresuz  46230  fouriersw  46677  fouriercn  46678  tposresg  49365  tposres3  49368