Theorem feqresmpt 6961

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 6758	. . 3 ⊢ (𝜑 → (𝐹 ↾ 𝐶):𝐶⟶𝐵)
4	3	feqmptd 6960	. 2 ⊢ (𝜑 → (𝐹 ↾ 𝐶) = (𝑥 ∈ 𝐶 ↦ ((𝐹 ↾ 𝐶)‘𝑥)))
5		fvres 6910	. . 3 ⊢ (𝑥 ∈ 𝐶 → ((𝐹 ↾ 𝐶)‘𝑥) = (𝐹‘𝑥))
6	5	mpteq2ia 5251	. 2 ⊢ (𝑥 ∈ 𝐶 ↦ ((𝐹 ↾ 𝐶)‘𝑥)) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))
7	4, 6	eqtrdi 2788	1 ⊢ (𝜑 → (𝐹 ↾ 𝐶) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)))

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3948   ↦ cmpt 5231   ↾ cres 5678  ⟶wf 6539  ‘cfv 6543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551

This theorem is referenced by:  pwfseqlem5  10660  pfxres  14631  gsumpt  19832  dpjidcl  19930  regsumsupp  21181  tsmsxplem2  23665  dvmulbr  25463  dvlip  25517  lhop1lem  25537  loglesqrt  26273  jensenlem1  26498  jensen  26500  amgm  26502  ushgredgedg  28524  ushgredgedgloop  28526  mgcf1o  32211  gsumzresunsn  32247  gsumpart  32248  gsumhashmul  32249  gsumle  32283  coinflippv  33551  fdvposlt  33680  fdvposle  33682  logdivsqrle  33731  gg-dvmulbr  35244  ftc1cnnclem  36645  dvasin  36658  dvacos  36659  dvreasin  36660  dvreacos  36661  areacirclem1  36662  dvrelog2  41015  dvrelog3  41016  cantnf2  42157  limsupvaluz2  44533  supcnvlimsup  44535  itgperiod  44776  fourierdlem69  44970  fourierdlem73  44974  fourierdlem74  44975  fourierdlem75  44976  fourierdlem76  44977  fourierdlem81  44982  fourierdlem85  44986  fourierdlem88  44989  fourierdlem92  44993  fourierdlem97  44998  fourierdlem100  45001  fourierdlem101  45002  fourierdlem103  45004  fourierdlem104  45005  fourierdlem107  45008  fourierdlem111  45012  fourierdlem112  45013  fouriersw  45026  sge0tsms  45175  sge0resrnlem  45198  meadjiunlem  45260  omeunle  45311  isomenndlem  45325