Theorem feqresmpt 6909

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 6707	. . 3 ⊢ (𝜑 → (𝐹 ↾ 𝐶):𝐶⟶𝐵)
4	3	feqmptd 6908	. 2 ⊢ (𝜑 → (𝐹 ↾ 𝐶) = (𝑥 ∈ 𝐶 ↦ ((𝐹 ↾ 𝐶)‘𝑥)))
5		fvres 6859	. . 3 ⊢ (𝑥 ∈ 𝐶 → ((𝐹 ↾ 𝐶)‘𝑥) = (𝐹‘𝑥))
6	5	mpteq2ia 5180	. 2 ⊢ (𝑥 ∈ 𝐶 ↦ ((𝐹 ↾ 𝐶)‘𝑥)) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))
7	4, 6	eqtrdi 2787	1 ⊢ (𝜑 → (𝐹 ↾ 𝐶) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)))

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3889   ↦ cmpt 5166   ↾ cres 5633  ⟶wf 6494  ‘cfv 6498

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-fv 6506

This theorem is referenced by:  pwfseqlem5  10586  pfxres  14642  gsumpt  19937  dpjidcl  20035  gsumle  20120  regsumsupp  21602  tsmsxplem2  24119  dvmulbr  25906  dvlip  25960  lhop1lem  25980  loglesqrt  26725  jensenlem1  26950  jensen  26952  amgm  26954  ushgredgedg  29298  ushgredgedgloop  29300  fisuppov1  32756  fmptunsnop  32773  mgcf1o  33063  gsumfs2d  33122  gsumzresunsn  33123  gsumpart  33124  gsumhashmul  33128  rprmdvdsprod  33594  coinflippv  34628  fdvposlt  34743  fdvposle  34745  logdivsqrle  34794  ftc1cnnclem  38012  dvasin  38025  dvacos  38026  dvreasin  38027  dvreacos  38028  areacirclem1  38029  dvrelog2  42503  dvrelog3  42504  aks6d1c2  42569  aks6d1c6lem3  42611  readvrec2  42793  readvrec  42794  resuppsinopn  42795  cantnf2  43753  limsupvaluz2  46166  supcnvlimsup  46168  itgperiod  46409  fourierdlem69  46603  fourierdlem73  46607  fourierdlem74  46608  fourierdlem75  46609  fourierdlem76  46610  fourierdlem81  46615  fourierdlem85  46619  fourierdlem88  46622  fourierdlem92  46626  fourierdlem97  46631  fourierdlem100  46634  fourierdlem101  46635  fourierdlem103  46637  fourierdlem104  46638  fourierdlem107  46641  fourierdlem111  46645  fourierdlem112  46646  fouriersw  46659  sge0tsms  46808  sge0resrnlem  46831  meadjiunlem  46893  omeunle  46944  isomenndlem  46958