Theorem resres 5116

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

Assertion

Ref	Expression
resres	|- ( ( A |` B ) |` C ) = ( A |` ( B i^i C ) )

Proof of Theorem resres

Step	Hyp	Ref	Expression
1		df-res 4845	. 2 |- ( ( A |` B ) |` C ) = ( ( A |` B ) i^i ( C X. _V ) )
2		df-res 4845	. . 3 |- ( A |` B ) = ( A i^i ( B X. _V ) )
3	2	ineq1i 3629	. 2 |- ( ( A |` B ) i^i ( C X. _V ) ) = ( ( A i^i ( B X. _V ) ) i^i ( C X. _V ) )
4		xpindir 4968	. . . 4 |- ( ( B i^i C ) X. _V ) = ( ( B X. _V ) i^i ( C X. _V ) )
5	4	ineq2i 3630	. . 3 |- ( A i^i ( ( B i^i C ) X. _V ) ) = ( A i^i ( ( B X. _V ) i^i ( C X. _V ) ) )
6		df-res 4845	. . 3 |- ( A |` ( B i^i C ) ) = ( A i^i ( ( B i^i C ) X. _V ) )
7		inass 3641	. . 3 |- ( ( A i^i ( B X. _V ) ) i^i ( C X. _V ) ) = ( A i^i ( ( B X. _V ) i^i ( C X. _V ) ) )
8	5, 6, 7	3eqtr4ri 2483	. 2 |- ( ( A i^i ( B X. _V ) ) i^i ( C X. _V ) ) = ( A |` ( B i^i C ) )
9	1, 3, 8	3eqtri 2476	1 |- ( ( A |` B ) |` C ) = ( A |` ( B i^i C ) )

Syntax hints:   = wceq 1443   _Vcvv 3044   i^i cin 3402   X. cxp 4831   |` cres 4835

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pr 4638

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-rex 2742  df-rab 2745  df-v 3046  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-sn 3968  df-pr 3970  df-op 3974  df-opab 4461  df-xp 4839  df-rel 4840  df-res 4845

This theorem is referenced by:  rescom  5128  resabs1  5132  resima2  5137  resmpt3  5154  resdisj  5265  rescnvcnv  5297  fresin  5750  resdif  5832  curry1  6885  curry2  6888  wfrlem4  7036  pmresg  7496  gruima  9224  rlimres  13615  lo1res  13616  rlimresb  13622  lo1eq  13625  rlimeq  13626  fsets  15142  setsid  15157  sscres  15721  gsumzres  17536  txkgen  20660  tsmsres  21151  ressxms  21533  ressms  21534  dvres  22859  dvres3a  22862  cpnres  22884  dvmptres3  22903  rlimcnp2  23885  df1stres  28277  df2ndres  28278  indf1ofs  28840  frrlem4  30510  dfrcl2  36260  relexpaddss  36304  fouriersw  38089  fouriercn  38090