Theorem feqresmpt 6978

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 6775	. . 3 ⊢ (𝜑 → (𝐹 ↾ 𝐶):𝐶⟶𝐵)
4	3	feqmptd 6977	. 2 ⊢ (𝜑 → (𝐹 ↾ 𝐶) = (𝑥 ∈ 𝐶 ↦ ((𝐹 ↾ 𝐶)‘𝑥)))
5		fvres 6925	. . 3 ⊢ (𝑥 ∈ 𝐶 → ((𝐹 ↾ 𝐶)‘𝑥) = (𝐹‘𝑥))
6	5	mpteq2ia 5245	. 2 ⊢ (𝑥 ∈ 𝐶 ↦ ((𝐹 ↾ 𝐶)‘𝑥)) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))
7	4, 6	eqtrdi 2793	1 ⊢ (𝜑 → (𝐹 ↾ 𝐶) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)))

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3951   ↦ cmpt 5225   ↾ cres 5687  ⟶wf 6557  ‘cfv 6561

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 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-fv 6569

This theorem is referenced by:  pwfseqlem5  10703  pfxres  14717  gsumpt  19980  dpjidcl  20078  regsumsupp  21640  tsmsxplem2  24162  dvmulbr  25975  dvmulbrOLD  25976  dvlip  26032  lhop1lem  26052  loglesqrt  26804  jensenlem1  27030  jensen  27032  amgm  27034  ushgredgedg  29246  ushgredgedgloop  29248  fisuppov1  32692  fmptunsnop  32709  mgcf1o  32993  gsumfs2d  33058  gsumzresunsn  33059  gsumpart  33060  gsumhashmul  33064  gsumle  33101  rprmdvdsprod  33562  coinflippv  34486  fdvposlt  34614  fdvposle  34616  logdivsqrle  34665  ftc1cnnclem  37698  dvasin  37711  dvacos  37712  dvreasin  37713  dvreacos  37714  areacirclem1  37715  dvrelog2  42065  dvrelog3  42066  aks6d1c2  42131  aks6d1c6lem3  42173  readvrec2  42391  readvrec  42392  resuppsinopn  42393  cantnf2  43338  limsupvaluz2  45753  supcnvlimsup  45755  itgperiod  45996  fourierdlem69  46190  fourierdlem73  46194  fourierdlem74  46195  fourierdlem75  46196  fourierdlem76  46197  fourierdlem81  46202  fourierdlem85  46206  fourierdlem88  46209  fourierdlem92  46213  fourierdlem97  46218  fourierdlem100  46221  fourierdlem101  46222  fourierdlem103  46224  fourierdlem104  46225  fourierdlem107  46228  fourierdlem111  46232  fourierdlem112  46233  fouriersw  46246  sge0tsms  46395  sge0resrnlem  46418  meadjiunlem  46480  omeunle  46531  isomenndlem  46545