Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > resres | Structured version Visualization version GIF version |
Description: The restriction of a restriction. (Contributed by NM, 27-Mar-2008.) |
Ref | Expression |
---|---|
resres | ⊢ ((𝐴 ↾ 𝐵) ↾ 𝐶) = (𝐴 ↾ (𝐵 ∩ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-res 5126 | . 2 ⊢ ((𝐴 ↾ 𝐵) ↾ 𝐶) = ((𝐴 ↾ 𝐵) ∩ (𝐶 × V)) | |
2 | df-res 5126 | . . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V)) | |
3 | 2 | ineq1i 3810 | . 2 ⊢ ((𝐴 ↾ 𝐵) ∩ (𝐶 × V)) = ((𝐴 ∩ (𝐵 × V)) ∩ (𝐶 × V)) |
4 | xpindir 5256 | . . . 4 ⊢ ((𝐵 ∩ 𝐶) × V) = ((𝐵 × V) ∩ (𝐶 × V)) | |
5 | 4 | ineq2i 3811 | . . 3 ⊢ (𝐴 ∩ ((𝐵 ∩ 𝐶) × V)) = (𝐴 ∩ ((𝐵 × V) ∩ (𝐶 × V))) |
6 | df-res 5126 | . . 3 ⊢ (𝐴 ↾ (𝐵 ∩ 𝐶)) = (𝐴 ∩ ((𝐵 ∩ 𝐶) × V)) | |
7 | inass 3823 | . . 3 ⊢ ((𝐴 ∩ (𝐵 × V)) ∩ (𝐶 × V)) = (𝐴 ∩ ((𝐵 × V) ∩ (𝐶 × V))) | |
8 | 5, 6, 7 | 3eqtr4ri 2655 | . 2 ⊢ ((𝐴 ∩ (𝐵 × V)) ∩ (𝐶 × V)) = (𝐴 ↾ (𝐵 ∩ 𝐶)) |
9 | 1, 3, 8 | 3eqtri 2648 | 1 ⊢ ((𝐴 ↾ 𝐵) ↾ 𝐶) = (𝐴 ↾ (𝐵 ∩ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1483 Vcvv 3200 ∩ cin 3573 × cxp 5112 ↾ cres 5116 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pr 4906 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-rab 2921 df-v 3202 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-opab 4713 df-xp 5120 df-rel 5121 df-res 5126 |
This theorem is referenced by: rescom 5423 resabs1 5427 resima2 5432 resima2OLD 5433 resmpt3 5450 resdisj 5563 rescnvcnv 5597 fresin 6073 resdif 6157 curry1 7269 curry2 7272 wfrlem4 7418 pmresg 7885 gruima 9624 rlimres 14289 lo1res 14290 rlimresb 14296 lo1eq 14299 rlimeq 14300 fsets 15891 setsid 15914 sscres 16483 gsumzres 18310 txkgen 21455 tsmsres 21947 ressxms 22330 ressms 22331 dvres 23675 dvres3a 23678 cpnres 23700 dvmptres3 23719 rlimcnp2 24693 df1stres 29481 df2ndres 29482 indf1ofs 30088 frrlem4 31783 dfrcl2 37966 relexpaddss 38010 limsupresuz 39935 liminfresuz 40016 fouriersw 40448 fouriercn 40449 |
Copyright terms: Public domain | W3C validator |