| 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 3960 | . 2 ⊢ 𝐵 ⊆ 𝐵 | |
| 2 | ressid.1 | . . 3 ⊢ 𝐵 = (Base‘𝑊) | |
| 3 | 2 | fvexi 6899 | . 2 ⊢ 𝐵 ∈ V |
| 4 | eqid 2765 | . . 3 ⊢ (𝑊 ↾s 𝐵) = (𝑊 ↾s 𝐵) | |
| 5 | 4, 2 | ressid2 17318 | . 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 2146 Vcvv 3457 ⊆ wss 3906 ‘cfv 6540 (class class class)co 7419 Basecbs 17293 ↾s cress 17314 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-sep 5259 ax-nul 5271 ax-pr 5406 |
| This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-ral 3082 df-rex 3092 df-rab 3419 df-v 3459 df-sbc 3747 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-nul 4287 df-if 4490 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4875 df-br 5112 df-opab 5176 df-id 5558 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-iota 6496 df-fun 6542 df-fv 6548 df-ov 7422 df-oprab 7423 df-mpo 7424 df-ress 17315 |
| This theorem is used by: ressval3d 17330 submgmid 18798 submid 18907 subgid 19240 gaid2 19419 subrngid 20700 subrgid 20724 sdrgid 20947 rlmval2 21365 rlmsca 21371 rlmsca2 21372 pjff 21914 dsmmfi 21940 frlmip 21980 evlrhm 22304 evlsscasrng 22308 evlsvarsrng 22310 evlsevl 22335 evlvvval 22336 evl1sca 22546 evl1var 22548 evls1scasrng 22551 evls1varsrng 22552 pf1ind 22567 evl1gsumadd 22570 evl1varpw 22573 ressply1evl 22582 cnstrcvs 25353 cncvs 25357 rlmbn 25573 ishl2 25582 rrxprds 25601 dchrptlem2 27482 evl1fpws 33920 evlextv 33998 resssra 34043 qusdimsum 34084 fldextid 34115 riccrng1 43349 ricdrng1 43356 evlvvvallem 43379 mhphf4 43392 lnmfg 43869 lmhmfgsplit 43873 pwslnmlem2 43880 simpcntrab 47644 |
| Copyright terms: Public domain | W3C validator |