Theorem feqresmpt 6838

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 6641	. . 3 ⊢ (𝜑 → (𝐹 ↾ 𝐶):𝐶⟶𝐵)
4	3	feqmptd 6837	. 2 ⊢ (𝜑 → (𝐹 ↾ 𝐶) = (𝑥 ∈ 𝐶 ↦ ((𝐹 ↾ 𝐶)‘𝑥)))
5		fvres 6793	. . 3 ⊢ (𝑥 ∈ 𝐶 → ((𝐹 ↾ 𝐶)‘𝑥) = (𝐹‘𝑥))
6	5	mpteq2ia 5177	. 2 ⊢ (𝑥 ∈ 𝐶 ↦ ((𝐹 ↾ 𝐶)‘𝑥)) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))
7	4, 6	eqtrdi 2794	1 ⊢ (𝜑 → (𝐹 ↾ 𝐶) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)))

Syntax hints:   → wi 4   = wceq 1539   ⊆ wss 3887   ↦ cmpt 5157   ↾ cres 5591  ⟶wf 6429  ‘cfv 6433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  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 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-fv 6441

This theorem is referenced by:  pwfseqlem5  10419  pfxres  14392  gsumpt  19563  dpjidcl  19661  regsumsupp  20827  tsmsxplem2  23305  dvmulbr  25103  dvlip  25157  lhop1lem  25177  loglesqrt  25911  jensenlem1  26136  jensen  26138  amgm  26140  ushgredgedg  27596  ushgredgedgloop  27598  mgcf1o  31281  gsumzresunsn  31314  gsumpart  31315  gsumhashmul  31316  gsumle  31350  coinflippv  32450  fdvposlt  32579  fdvposle  32581  logdivsqrle  32630  ftc1cnnclem  35848  dvasin  35861  dvacos  35862  dvreasin  35863  dvreacos  35864  areacirclem1  35865  dvrelog2  40072  dvrelog3  40073  limsupvaluz2  43279  supcnvlimsup  43281  itgperiod  43522  fourierdlem69  43716  fourierdlem73  43720  fourierdlem74  43721  fourierdlem75  43722  fourierdlem76  43723  fourierdlem81  43728  fourierdlem85  43732  fourierdlem88  43735  fourierdlem92  43739  fourierdlem97  43744  fourierdlem100  43747  fourierdlem101  43748  fourierdlem103  43750  fourierdlem104  43751  fourierdlem107  43754  fourierdlem111  43758  fourierdlem112  43759  fouriersw  43772  sge0tsms  43918  sge0resrnlem  43941  meadjiunlem  44003  omeunle  44054  isomenndlem  44068