Theorem feqresmpt 6948

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 6745	. . 3 ⊢ (𝜑 → (𝐹 ↾ 𝐶):𝐶⟶𝐵)
4	3	feqmptd 6947	. 2 ⊢ (𝜑 → (𝐹 ↾ 𝐶) = (𝑥 ∈ 𝐶 ↦ ((𝐹 ↾ 𝐶)‘𝑥)))
5		fvres 6895	. . 3 ⊢ (𝑥 ∈ 𝐶 → ((𝐹 ↾ 𝐶)‘𝑥) = (𝐹‘𝑥))
6	5	mpteq2ia 5216	. 2 ⊢ (𝑥 ∈ 𝐶 ↦ ((𝐹 ↾ 𝐶)‘𝑥)) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))
7	4, 6	eqtrdi 2786	1 ⊢ (𝜑 → (𝐹 ↾ 𝐶) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)))

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3926   ↦ cmpt 5201   ↾ cres 5656  ⟶wf 6527  ‘cfv 6531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-fv 6539

This theorem is referenced by:  pwfseqlem5  10677  pfxres  14697  gsumpt  19943  dpjidcl  20041  regsumsupp  21582  tsmsxplem2  24092  dvmulbr  25893  dvmulbrOLD  25894  dvlip  25950  lhop1lem  25970  loglesqrt  26723  jensenlem1  26949  jensen  26951  amgm  26953  ushgredgedg  29208  ushgredgedgloop  29210  fisuppov1  32660  fmptunsnop  32677  mgcf1o  32983  gsumfs2d  33049  gsumzresunsn  33050  gsumpart  33051  gsumhashmul  33055  gsumle  33092  rprmdvdsprod  33549  coinflippv  34516  fdvposlt  34631  fdvposle  34633  logdivsqrle  34682  ftc1cnnclem  37715  dvasin  37728  dvacos  37729  dvreasin  37730  dvreacos  37731  areacirclem1  37732  dvrelog2  42077  dvrelog3  42078  aks6d1c2  42143  aks6d1c6lem3  42185  readvrec2  42404  readvrec  42405  resuppsinopn  42406  cantnf2  43349  limsupvaluz2  45767  supcnvlimsup  45769  itgperiod  46010  fourierdlem69  46204  fourierdlem73  46208  fourierdlem74  46209  fourierdlem75  46210  fourierdlem76  46211  fourierdlem81  46216  fourierdlem85  46220  fourierdlem88  46223  fourierdlem92  46227  fourierdlem97  46232  fourierdlem100  46235  fourierdlem101  46236  fourierdlem103  46238  fourierdlem104  46239  fourierdlem107  46242  fourierdlem111  46246  fourierdlem112  46247  fouriersw  46260  sge0tsms  46409  sge0resrnlem  46432  meadjiunlem  46494  omeunle  46545  isomenndlem  46559