Theorem feqresmpt 6947

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 6744	. . 3 ⊢ (𝜑 → (𝐹 ↾ 𝐶):𝐶⟶𝐵)
4	3	feqmptd 6946	. 2 ⊢ (𝜑 → (𝐹 ↾ 𝐶) = (𝑥 ∈ 𝐶 ↦ ((𝐹 ↾ 𝐶)‘𝑥)))
5		fvres 6894	. . 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 6526  ‘cfv 6530

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 6483  df-fun 6532  df-fn 6533  df-f 6534  df-fv 6538

This theorem is referenced by:  pwfseqlem5  10675  pfxres  14695  gsumpt  19941  dpjidcl  20039  regsumsupp  21580  tsmsxplem2  24090  dvmulbr  25891  dvmulbrOLD  25892  dvlip  25948  lhop1lem  25968  loglesqrt  26721  jensenlem1  26947  jensen  26949  amgm  26951  ushgredgedg  29154  ushgredgedgloop  29156  fisuppov1  32606  fmptunsnop  32623  mgcf1o  32929  gsumfs2d  32995  gsumzresunsn  32996  gsumpart  32997  gsumhashmul  33001  gsumle  33038  rprmdvdsprod  33495  coinflippv  34462  fdvposlt  34577  fdvposle  34579  logdivsqrle  34628  ftc1cnnclem  37661  dvasin  37674  dvacos  37675  dvreasin  37676  dvreacos  37677  areacirclem1  37678  dvrelog2  42023  dvrelog3  42024  aks6d1c2  42089  aks6d1c6lem3  42131  readvrec2  42351  readvrec  42352  resuppsinopn  42353  cantnf2  43296  limsupvaluz2  45715  supcnvlimsup  45717  itgperiod  45958  fourierdlem69  46152  fourierdlem73  46156  fourierdlem74  46157  fourierdlem75  46158  fourierdlem76  46159  fourierdlem81  46164  fourierdlem85  46168  fourierdlem88  46171  fourierdlem92  46175  fourierdlem97  46180  fourierdlem100  46183  fourierdlem101  46184  fourierdlem103  46186  fourierdlem104  46187  fourierdlem107  46190  fourierdlem111  46194  fourierdlem112  46195  fouriersw  46208  sge0tsms  46357  sge0resrnlem  46380  meadjiunlem  46442  omeunle  46493  isomenndlem  46507