| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > ressid | Structured version Visualization version GIF version | ||
| Description: Behavior of trivial restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.) |
| Ref | Expression |
|---|---|
| ressid.1 | ⊢ 𝐵 = (Base‘𝑊) |
| Ref | Expression |
|---|---|
| ressid | ⊢ (𝑊 ∈ 𝑋 → (𝑊 ↾s 𝐵) = 𝑊) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ssid 3959 | . 2 ⊢ 𝐵 ⊆ 𝐵 | |
| 2 | ressid.1 | . . 3 ⊢ 𝐵 = (Base‘𝑊) | |
| 3 | 2 | fvexi 6895 | . 2 ⊢ 𝐵 ∈ V |
| 4 | eqid 2763 | . . 3 ⊢ (𝑊 ↾s 𝐵) = (𝑊 ↾s 𝐵) | |
| 5 | 4, 2 | ressid2 17298 | . 2 ⊢ ((𝐵 ⊆ 𝐵 ∧ 𝑊 ∈ 𝑋 ∧ 𝐵 ∈ V) → (𝑊 ↾s 𝐵) = 𝑊) |
| 6 | 1, 3, 5 | mp3an13 1481 | 1 ⊢ (𝑊 ∈ 𝑋 → (𝑊 ↾s 𝐵) = 𝑊) |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: → wi 4 = wceq 1570 ∈ wcel 2143 Vcvv 3455 ⊆ wss 3905 ‘cfv 6536 (class class class)co 7410 Basecbs 17273 ↾s cress 17294 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-sep 5257 ax-nul 5269 ax-pr 5404 |
| This proof depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-ral 3080 df-rex 3090 df-rab 3417 df-v 3457 df-sbc 3745 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-nul 4287 df-if 4488 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4873 df-br 5110 df-opab 5174 df-id 5556 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-iota 6492 df-fun 6538 df-fv 6544 df-ov 7413 df-oprab 7414 df-mpo 7415 df-ress 17295 |
| This theorem is used by: ressval3d 17310 submgmid 18768 submid 18872 subgid 19198 gaid2 19377 subrngid 20657 subrgid 20681 sdrgid 20904 rlmval2 21322 rlmsca 21328 rlmsca2 21329 pjff 21871 dsmmfi 21897 frlmip 21937 evlrhm 22261 evlsscasrng 22265 evlsvarsrng 22267 evlsevl 22292 evlvvval 22293 evl1sca 22503 evl1var 22505 evls1scasrng 22508 evls1varsrng 22509 pf1ind 22524 evl1gsumadd 22527 evl1varpw 22530 ressply1evl 22539 cnstrcvs 25309 cncvs 25313 rlmbn 25529 ishl2 25538 rrxprds 25557 dchrptlem2 27438 evl1fpws 33863 evlextv 33941 resssra 33986 qusdimsum 34027 fldextid 34058 riccrng1 43317 ricdrng1 43324 evlvvvallem 43347 mhphf4 43360 lnmfg 43837 lmhmfgsplit 43841 pwslnmlem2 43848 simpcntrab 47612 |
| Copyright terms: Public domain | W3C validator |