Theorem feqresmpt 6952

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 6747	. . 3 ⊢ (𝜑 → (𝐹 ↾ 𝐶):𝐶⟶𝐵)
4	3	feqmptd 6951	. 2 ⊢ (𝜑 → (𝐹 ↾ 𝐶) = (𝑥 ∈ 𝐶 ↦ ((𝐹 ↾ 𝐶)‘𝑥)))
5		fvres 6902	. . 3 ⊢ (𝑥 ∈ 𝐶 → ((𝐹 ↾ 𝐶)‘𝑥) = (𝐹‘𝑥))
6	5	mpteq2ia 5200	. 2 ⊢ (𝑥 ∈ 𝐶 ↦ ((𝐹 ↾ 𝐶)‘𝑥)) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))
7	4, 6	eqtrdi 2812	1 ⊢ (𝜑 → (𝐹 ↾ 𝐶) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)))

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3899   ↦ cmpt 5186   ↾ cres 5653  ⟶wf 6533  ‘cfv 6537

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-fv 6545

This theorem is used by:  pwfseqlem5  10741  pfxres  14822  gsumpt  20169  dpjidcl  20267  gsumle  20352  regsumsupp  21921  tsmsxplem2  24466  dvmulbr  26252  dvlip  26306  lhop1lem  26326  loglesqrt  27082  jensenlem1  27307  jensen  27309  amgm  27311  ushgredgedg  29803  ushgredgedgloop  29805  fisuppov1  33269  fmptunsnop  33286  mgcf1o  33557  gsumfs2d  33615  gsumzresunsn  33616  gsumpart  33617  gsumhashmul  33621  rprmdvdsprod  34059  coinflippv  35109  fdvposlt  35221  fdvposle  35223  logdivsqrle  35272  ftc1cnnclem  38589  dvasin  38602  dvacos  38603  dvreasin  38604  dvreacos  38605  areacirclem1  38606  dvrelog2  43094  dvrelog3  43095  aks6d1c2  43160  aks6d1c6lem3  43202  readvrec2  43392  readvrec  43393  resuppsinopn  43394  cantnf2  44311  limsupvaluz2  46717  supcnvlimsup  46719  itgperiod  46960  fourierdlem69  47154  fourierdlem73  47158  fourierdlem74  47159  fourierdlem75  47160  fourierdlem76  47161  fourierdlem81  47166  fourierdlem85  47170  fourierdlem88  47173  fourierdlem92  47177  fourierdlem97  47182  fourierdlem100  47185  fourierdlem101  47186  fourierdlem103  47188  fourierdlem104  47189  fourierdlem107  47192  fourierdlem111  47196  fourierdlem112  47197  fouriersw  47210  sge0tsms  47359  sge0resrnlem  47382  meadjiunlem  47444  omeunle  47495  isomenndlem  47509