![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > feqresmpt | Structured version Visualization version GIF version |
Description: Express a restricted function as a mapping. (Contributed by Mario Carneiro, 18-May-2016.) |
Ref | Expression |
---|---|
feqmptd.1 | ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
feqresmpt.2 | ⊢ (𝜑 → 𝐶 ⊆ 𝐴) |
Ref | Expression |
---|---|
feqresmpt | ⊢ (𝜑 → (𝐹 ↾ 𝐶) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | feqmptd.1 | . . . 4 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) | |
2 | feqresmpt.2 | . . . 4 ⊢ (𝜑 → 𝐶 ⊆ 𝐴) | |
3 | 1, 2 | fssresd 6413 | . . 3 ⊢ (𝜑 → (𝐹 ↾ 𝐶):𝐶⟶𝐵) |
4 | 3 | feqmptd 6601 | . 2 ⊢ (𝜑 → (𝐹 ↾ 𝐶) = (𝑥 ∈ 𝐶 ↦ ((𝐹 ↾ 𝐶)‘𝑥))) |
5 | fvres 6557 | . . 3 ⊢ (𝑥 ∈ 𝐶 → ((𝐹 ↾ 𝐶)‘𝑥) = (𝐹‘𝑥)) | |
6 | 5 | mpteq2ia 5051 | . 2 ⊢ (𝑥 ∈ 𝐶 ↦ ((𝐹 ↾ 𝐶)‘𝑥)) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) |
7 | 4, 6 | syl6eq 2847 | 1 ⊢ (𝜑 → (𝐹 ↾ 𝐶) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1522 ⊆ wss 3859 ↦ cmpt 5041 ↾ cres 5445 ⟶wf 6221 ‘cfv 6225 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-sep 5094 ax-nul 5101 ax-pr 5221 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ral 3110 df-rex 3111 df-rab 3114 df-v 3439 df-sbc 3707 df-dif 3862 df-un 3864 df-in 3866 df-ss 3874 df-nul 4212 df-if 4382 df-sn 4473 df-pr 4475 df-op 4479 df-uni 4746 df-br 4963 df-opab 5025 df-mpt 5042 df-id 5348 df-xp 5449 df-rel 5450 df-cnv 5451 df-co 5452 df-dm 5453 df-rn 5454 df-res 5455 df-iota 6189 df-fun 6227 df-fn 6228 df-f 6229 df-fv 6233 |
This theorem is referenced by: pwfseqlem5 9931 pfxres 13877 gsumpt 18802 dpjidcl 18897 regsumsupp 20448 tsmsxplem2 22445 dvmulbr 24219 dvlip 24273 lhop1lem 24293 loglesqrt 25020 jensenlem1 25246 jensen 25248 amgm 25250 ushgredgedg 26694 ushgredgedgloop 26696 gsumle 30494 gsumzresunsn 30502 coinflippv 31358 fdvposlt 31487 fdvposle 31489 logdivsqrle 31538 ftc1cnnclem 34496 dvasin 34509 dvacos 34510 dvreasin 34511 dvreacos 34512 areacirclem1 34513 limsupvaluz2 41561 supcnvlimsup 41563 itgperiod 41807 fourierdlem69 42002 fourierdlem73 42006 fourierdlem74 42007 fourierdlem75 42008 fourierdlem76 42009 fourierdlem81 42014 fourierdlem85 42018 fourierdlem88 42021 fourierdlem92 42025 fourierdlem97 42030 fourierdlem100 42033 fourierdlem101 42034 fourierdlem103 42036 fourierdlem104 42037 fourierdlem107 42040 fourierdlem111 42044 fourierdlem112 42045 fouriersw 42058 sge0tsms 42204 sge0resrnlem 42227 meadjiunlem 42289 omeunle 42340 isomenndlem 42354 |
Copyright terms: Public domain | W3C validator |