Theorem feqresmpt 6899

Description: Express a restricted function as a mapping. (Contributed by Mario Carneiro, 18-May-2016.)

Hypotheses

Ref	Expression
feqmptd.1	⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
feqresmpt.2	⊢ (𝜑 → 𝐶 ⊆ 𝐴)

Assertion

Ref	Expression
feqresmpt	⊢ (𝜑 → (𝐹 ↾ 𝐶) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐶   𝑥,𝐹

Allowed substitution hints:   𝜑(𝑥)   𝐵(𝑥)

Proof of Theorem feqresmpt

Step	Hyp	Ref	Expression
1		feqmptd.1	. . . 4 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
2		feqresmpt.2	. . . 4 ⊢ (𝜑 → 𝐶 ⊆ 𝐴)
3	1, 2	fssresd 6697	. . 3 ⊢ (𝜑 → (𝐹 ↾ 𝐶):𝐶⟶𝐵)
4	3	feqmptd 6898	. 2 ⊢ (𝜑 → (𝐹 ↾ 𝐶) = (𝑥 ∈ 𝐶 ↦ ((𝐹 ↾ 𝐶)‘𝑥)))
5		fvres 6849	. . 3 ⊢ (𝑥 ∈ 𝐶 → ((𝐹 ↾ 𝐶)‘𝑥) = (𝐹‘𝑥))
6	5	mpteq2ia 5169	. 2 ⊢ (𝑥 ∈ 𝐶 ↦ ((𝐹 ↾ 𝐶)‘𝑥)) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))
7	4, 6	eqtrdi 2792	1 ⊢ (𝜑 → (𝐹 ↾ 𝐶) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)))

Syntax hints:   → wi 4   = wceq 1548   ⊆ wss 3884   ↦ cmpt 5155   ↾ cres 5622  ⟶wf 6484  ‘cfv 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-sep 5220  ax-nul 5230  ax-pr 5364

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4264  df-if 4457  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-br 5075  df-opab 5137  df-mpt 5156  df-id 5515  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-iota 6444  df-fun 6490  df-fn 6491  df-f 6492  df-fv 6496

This theorem is referenced by:  pwfseqlem5  10582  pfxres  14637  gsumpt  19931  dpjidcl  20029  gsumle  20114  regsumsupp  21600  tsmsxplem2  24140  dvmulbr  25927  dvlip  25981  lhop1lem  26001  loglesqrt  26746  jensenlem1  26971  jensen  26973  amgm  26975  ushgredgedg  29318  ushgredgedgloop  29320  fisuppov1  32777  fmptunsnop  32794  mgcf1o  33084  gsumfs2d  33144  gsumzresunsn  33145  gsumpart  33146  gsumhashmul  33150  rprmdvdsprod  33627  coinflippv  34678  fdvposlt  34793  fdvposle  34795  logdivsqrle  34844  ftc1cnnclem  38071  dvasin  38084  dvacos  38085  dvreasin  38086  dvreacos  38087  areacirclem1  38088  dvrelog2  42562  dvrelog3  42563  aks6d1c2  42628  aks6d1c6lem3  42670  readvrec2  42851  readvrec  42852  resuppsinopn  42853  cantnf2  43783  limsupvaluz2  46193  supcnvlimsup  46195  itgperiod  46436  fourierdlem69  46630  fourierdlem73  46634  fourierdlem74  46635  fourierdlem75  46636  fourierdlem76  46637  fourierdlem81  46642  fourierdlem85  46646  fourierdlem88  46649  fourierdlem92  46653  fourierdlem97  46658  fourierdlem100  46661  fourierdlem101  46662  fourierdlem103  46664  fourierdlem104  46665  fourierdlem107  46668  fourierdlem111  46672  fourierdlem112  46673  fouriersw  46686  sge0tsms  46835  sge0resrnlem  46858  meadjiunlem  46920  omeunle  46971  isomenndlem  46985