![]() |
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 5701 | . 2 ⊢ ((𝐴 ↾ 𝐵) ↾ 𝐶) = ((𝐴 ↾ 𝐵) ∩ (𝐶 × V)) | |
2 | df-res 5701 | . . 3 ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V)) | |
3 | 2 | ineq1i 4224 | . 2 ⊢ ((𝐴 ↾ 𝐵) ∩ (𝐶 × V)) = ((𝐴 ∩ (𝐵 × V)) ∩ (𝐶 × V)) |
4 | xpindir 5848 | . . . 4 ⊢ ((𝐵 ∩ 𝐶) × V) = ((𝐵 × V) ∩ (𝐶 × V)) | |
5 | 4 | ineq2i 4225 | . . 3 ⊢ (𝐴 ∩ ((𝐵 ∩ 𝐶) × V)) = (𝐴 ∩ ((𝐵 × V) ∩ (𝐶 × V))) |
6 | df-res 5701 | . . 3 ⊢ (𝐴 ↾ (𝐵 ∩ 𝐶)) = (𝐴 ∩ ((𝐵 ∩ 𝐶) × V)) | |
7 | inass 4236 | . . 3 ⊢ ((𝐴 ∩ (𝐵 × V)) ∩ (𝐶 × V)) = (𝐴 ∩ ((𝐵 × V) ∩ (𝐶 × V))) | |
8 | 5, 6, 7 | 3eqtr4ri 2774 | . 2 ⊢ ((𝐴 ∩ (𝐵 × V)) ∩ (𝐶 × V)) = (𝐴 ↾ (𝐵 ∩ 𝐶)) |
9 | 1, 3, 8 | 3eqtri 2767 | 1 ⊢ ((𝐴 ↾ 𝐵) ↾ 𝐶) = (𝐴 ↾ (𝐵 ∩ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1537 Vcvv 3478 ∩ cin 3962 × cxp 5687 ↾ cres 5691 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 ax-sep 5302 ax-nul 5312 ax-pr 5438 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1540 df-fal 1550 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-ral 3060 df-rex 3069 df-rab 3434 df-v 3480 df-dif 3966 df-un 3968 df-in 3970 df-ss 3980 df-nul 4340 df-if 4532 df-sn 4632 df-pr 4634 df-op 4638 df-opab 5211 df-xp 5695 df-rel 5696 df-res 5701 |
This theorem is referenced by: rescom 6023 resabs1 6027 resima2 6036 resmpt3 6058 resdisj 6191 rescnvcnv 6226 fresin 6778 resdif 6870 curry1 8128 curry2 8131 frrlem4 8313 wfrlem4OLD 8351 pmresg 8909 gruima 10840 rlimres 15591 lo1res 15592 rlimresb 15598 lo1eq 15601 rlimeq 15602 fsets 17203 setsid 17242 sscres 17871 gsumzres 19942 txkgen 23676 tsmsres 24168 ressxms 24554 ressms 24555 dvres 25961 dvres3a 25964 cpnres 25988 dvmptres3 26009 rlimcnp2 27024 df1stres 32719 df2ndres 32720 indf1ofs 34007 dfrcl2 43664 relexpaddss 43708 limsupresuz 45659 liminfresuz 45740 fouriersw 46187 fouriercn 46188 |
Copyright terms: Public domain | W3C validator |