Theorem resres 6002

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 5694	. 2 ⊢ ((𝐴 ↾ 𝐵) ↾ 𝐶) = ((𝐴 ↾ 𝐵) ∩ (𝐶 × V))
2		df-res 5694	. . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V))
3	2	ineq1i 4210	. 2 ⊢ ((𝐴 ↾ 𝐵) ∩ (𝐶 × V)) = ((𝐴 ∩ (𝐵 × V)) ∩ (𝐶 × V))
4		xpindir 5841	. . . 4 ⊢ ((𝐵 ∩ 𝐶) × V) = ((𝐵 × V) ∩ (𝐶 × V))
5	4	ineq2i 4211	. . 3 ⊢ (𝐴 ∩ ((𝐵 ∩ 𝐶) × V)) = (𝐴 ∩ ((𝐵 × V) ∩ (𝐶 × V)))
6		df-res 5694	. . 3 ⊢ (𝐴 ↾ (𝐵 ∩ 𝐶)) = (𝐴 ∩ ((𝐵 ∩ 𝐶) × V))
7		inass 4222	. . 3 ⊢ ((𝐴 ∩ (𝐵 × V)) ∩ (𝐶 × V)) = (𝐴 ∩ ((𝐵 × V) ∩ (𝐶 × V)))
8	5, 6, 7	3eqtr4ri 2767	. 2 ⊢ ((𝐴 ∩ (𝐵 × V)) ∩ (𝐶 × V)) = (𝐴 ↾ (𝐵 ∩ 𝐶))
9	1, 3, 8	3eqtri 2760	1 ⊢ ((𝐴 ↾ 𝐵) ↾ 𝐶) = (𝐴 ↾ (𝐵 ∩ 𝐶))

Syntax hints:   = wceq 1533  Vcvv 3473   ∩ cin 3948   × cxp 5680   ↾ cres 5684

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pr 5433

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-ral 3059  df-rex 3068  df-rab 3431  df-v 3475  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-sn 4633  df-pr 4635  df-op 4639  df-opab 5215  df-xp 5688  df-rel 5689  df-res 5694

This theorem is referenced by:  rescom  6012  resabs1  6016  resima2  6025  resmpt3  6047  resdisj  6178  rescnvcnv  6213  fresin  6771  resdif  6865  curry1  8115  curry2  8118  frrlem4  8301  wfrlem4OLD  8339  pmresg  8895  gruima  10833  rlimres  15542  lo1res  15543  rlimresb  15549  lo1eq  15552  rlimeq  15553  fsets  17145  setsid  17184  sscres  17813  gsumzres  19871  txkgen  23576  tsmsres  24068  ressxms  24454  ressms  24455  dvres  25860  dvres3a  25863  cpnres  25887  dvmptres3  25908  rlimcnp2  26918  df1stres  32504  df2ndres  32505  indf1ofs  33678  dfrcl2  43135  relexpaddss  43179  limsupresuz  45120  liminfresuz  45201  fouriersw  45648  fouriercn  45649