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  10657  pfxres  14628  gsumpt  19829  dpjidcl  19927  regsumsupp  21174  tsmsxplem2  23657  dvmulbr  25455  dvlip  25509  lhop1lem  25529  loglesqrt  26263  jensenlem1  26488  jensen  26490  amgm  26492  ushgredgedg  28483  ushgredgedgloop  28485  mgcf1o  32168  gsumzresunsn  32201  gsumpart  32202  gsumhashmul  32203  gsumle  32237  coinflippv  33477  fdvposlt  33606  fdvposle  33608  logdivsqrle  33657  gg-dvmulbr  35170  ftc1cnnclem  36554  dvasin  36567  dvacos  36568  dvreasin  36569  dvreacos  36570  areacirclem1  36571  dvrelog2  40924  dvrelog3  40925  cantnf2  42065  limsupvaluz2  44444  supcnvlimsup  44446  itgperiod  44687  fourierdlem69  44881  fourierdlem73  44885  fourierdlem74  44886  fourierdlem75  44887  fourierdlem76  44888  fourierdlem81  44893  fourierdlem85  44897  fourierdlem88  44900  fourierdlem92  44904  fourierdlem97  44909  fourierdlem100  44912  fourierdlem101  44913  fourierdlem103  44915  fourierdlem104  44916  fourierdlem107  44919  fourierdlem111  44923  fourierdlem112  44924  fouriersw  44937  sge0tsms  45086  sge0resrnlem  45109  meadjiunlem  45171  omeunle  45222  isomenndlem  45236