![]() |
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 6764 | . . 3 ⊢ (𝜑 → (𝐹 ↾ 𝐶):𝐶⟶𝐵) |
4 | 3 | feqmptd 6966 | . 2 ⊢ (𝜑 → (𝐹 ↾ 𝐶) = (𝑥 ∈ 𝐶 ↦ ((𝐹 ↾ 𝐶)‘𝑥))) |
5 | fvres 6915 | . . 3 ⊢ (𝑥 ∈ 𝐶 → ((𝐹 ↾ 𝐶)‘𝑥) = (𝐹‘𝑥)) | |
6 | 5 | mpteq2ia 5252 | . 2 ⊢ (𝑥 ∈ 𝐶 ↦ ((𝐹 ↾ 𝐶)‘𝑥)) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)) |
7 | 4, 6 | eqtrdi 2781 | 1 ⊢ (𝜑 → (𝐹 ↾ 𝐶) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1533 ⊆ wss 3944 ↦ cmpt 5232 ↾ cres 5680 ⟶wf 6545 ‘cfv 6549 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-sep 5300 ax-nul 5307 ax-pr 5429 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ne 2930 df-ral 3051 df-rex 3060 df-rab 3419 df-v 3463 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4323 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4910 df-br 5150 df-opab 5212 df-mpt 5233 df-id 5576 df-xp 5684 df-rel 5685 df-cnv 5686 df-co 5687 df-dm 5688 df-rn 5689 df-res 5690 df-iota 6501 df-fun 6551 df-fn 6552 df-f 6553 df-fv 6557 |
This theorem is referenced by: pwfseqlem5 10688 pfxres 14665 gsumpt 19929 dpjidcl 20027 regsumsupp 21571 tsmsxplem2 24102 dvmulbr 25913 dvmulbrOLD 25914 dvlip 25970 lhop1lem 25990 loglesqrt 26738 jensenlem1 26964 jensen 26966 amgm 26968 ushgredgedg 29114 ushgredgedgloop 29116 mgcf1o 32819 gsumzresunsn 32858 gsumpart 32859 gsumhashmul 32860 gsumle 32894 rprmdvdsprod 33346 coinflippv 34234 fdvposlt 34362 fdvposle 34364 logdivsqrle 34413 ftc1cnnclem 37295 dvasin 37308 dvacos 37309 dvreasin 37310 dvreacos 37311 areacirclem1 37312 dvrelog2 41667 dvrelog3 41668 aks6d1c2 41733 aks6d1c6lem3 41775 cantnf2 42896 limsupvaluz2 45264 supcnvlimsup 45266 itgperiod 45507 fourierdlem69 45701 fourierdlem73 45705 fourierdlem74 45706 fourierdlem75 45707 fourierdlem76 45708 fourierdlem81 45713 fourierdlem85 45717 fourierdlem88 45720 fourierdlem92 45724 fourierdlem97 45729 fourierdlem100 45732 fourierdlem101 45733 fourierdlem103 45735 fourierdlem104 45736 fourierdlem107 45739 fourierdlem111 45743 fourierdlem112 45744 fouriersw 45757 sge0tsms 45906 sge0resrnlem 45929 meadjiunlem 45991 omeunle 46042 isomenndlem 46056 |
Copyright terms: Public domain | W3C validator |