![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fvresi | Structured version Visualization version GIF version |
Description: The value of a restricted identity function. (Contributed by NM, 19-May-2004.) |
Ref | Expression |
---|---|
fvresi | ⊢ (𝐵 ∈ 𝐴 → (( I ↾ 𝐴)‘𝐵) = 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fvres 6245 | . 2 ⊢ (𝐵 ∈ 𝐴 → (( I ↾ 𝐴)‘𝐵) = ( I ‘𝐵)) | |
2 | fvi 6294 | . 2 ⊢ (𝐵 ∈ 𝐴 → ( I ‘𝐵) = 𝐵) | |
3 | 1, 2 | eqtrd 2685 | 1 ⊢ (𝐵 ∈ 𝐴 → (( I ↾ 𝐴)‘𝐵) = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1523 ∈ wcel 2030 I cid 5052 ↾ cres 5145 ‘cfv 5926 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 ax-sep 4814 ax-nul 4822 ax-pr 4936 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1056 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-eu 2502 df-mo 2503 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-ral 2946 df-rex 2947 df-rab 2950 df-v 3233 df-sbc 3469 df-dif 3610 df-un 3612 df-in 3614 df-ss 3621 df-nul 3949 df-if 4120 df-sn 4211 df-pr 4213 df-op 4217 df-uni 4469 df-br 4686 df-opab 4746 df-id 5053 df-xp 5149 df-rel 5150 df-cnv 5151 df-co 5152 df-dm 5153 df-res 5155 df-iota 5889 df-fun 5928 df-fv 5934 |
This theorem is referenced by: fninfp 6481 fndifnfp 6483 fnnfpeq0 6485 f1ocnvfv1 6572 f1ocnvfv2 6573 fcof1 6582 fcofo 6583 isoid 6619 weniso 6644 iordsmo 7499 fipreima 8313 infxpenc 8879 dfac9 8996 fproddvdsd 15106 ndxarg 15929 idfu2 16585 idfu1 16587 idfucl 16588 cofurid 16598 funcestrcsetclem6 16832 funcestrcsetclem7 16833 funcestrcsetclem9 16835 funcsetcestrclem6 16847 funcsetcestrclem7 16848 funcsetcestrclem9 16850 yonedainv 16968 idmhm 17391 idghm 17722 lactghmga 17870 symgga 17872 cayleylem2 17879 gsmsymgrfix 17894 gsmsymgreq 17898 pmtrfinv 17927 idlmhm 19089 evl1vard 19749 islinds2 20200 lindsind2 20206 madetsumid 20315 mdetunilem7 20472 txkgen 21503 ustuqtop3 22094 iducn 22134 nmoid 22593 dvid 23726 mvth 23800 fta1blem 23973 qaa 24123 idmot 25477 dfiop2 28740 idunop 28965 idcnop 28968 elunop2 29000 lnophm 29006 pmtridfv1 29985 pmtridfv2 29986 qqhre 30192 subfacp1lem4 31291 subfacp1lem5 31292 cvmliftlem5 31397 bj-evalid 33153 idlaut 35700 idldil 35718 ltrnid 35739 idltrn 35754 ltrnideq 35780 tendoidcl 36374 tendo1ne0 36433 cdleml7 36587 tendospid 36623 dvalveclem 36631 rngunsnply 38060 idmgmhm 42113 funcrngcsetcALT 42324 funcringcsetcALTV2lem6 42366 funcringcsetcALTV2lem7 42367 funcringcsetcALTV2lem9 42369 funcringcsetclem6ALTV 42389 funcringcsetclem7ALTV 42390 funcringcsetclem9ALTV 42392 dflinc2 42524 |
Copyright terms: Public domain | W3C validator |