Theorem feqresmpt 6930

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 6727	. . 3 ⊢ (𝜑 → (𝐹 ↾ 𝐶):𝐶⟶𝐵)
4	3	feqmptd 6929	. 2 ⊢ (𝜑 → (𝐹 ↾ 𝐶) = (𝑥 ∈ 𝐶 ↦ ((𝐹 ↾ 𝐶)‘𝑥)))
5		fvres 6877	. . 3 ⊢ (𝑥 ∈ 𝐶 → ((𝐹 ↾ 𝐶)‘𝑥) = (𝐹‘𝑥))
6	5	mpteq2ia 5202	. 2 ⊢ (𝑥 ∈ 𝐶 ↦ ((𝐹 ↾ 𝐶)‘𝑥)) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥))
7	4, 6	eqtrdi 2780	1 ⊢ (𝜑 → (𝐹 ↾ 𝐶) = (𝑥 ∈ 𝐶 ↦ (𝐹‘𝑥)))

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3914   ↦ cmpt 5188   ↾ cres 5640  ⟶wf 6507  ‘cfv 6511

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

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 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-fv 6519

This theorem is referenced by:  pwfseqlem5  10616  pfxres  14644  gsumpt  19892  dpjidcl  19990  regsumsupp  21531  tsmsxplem2  24041  dvmulbr  25841  dvmulbrOLD  25842  dvlip  25898  lhop1lem  25918  loglesqrt  26671  jensenlem1  26897  jensen  26899  amgm  26901  ushgredgedg  29156  ushgredgedgloop  29158  fisuppov1  32606  fmptunsnop  32623  mgcf1o  32929  gsumfs2d  32995  gsumzresunsn  32996  gsumpart  32997  gsumhashmul  33001  gsumle  33038  rprmdvdsprod  33505  coinflippv  34475  fdvposlt  34590  fdvposle  34592  logdivsqrle  34641  ftc1cnnclem  37685  dvasin  37698  dvacos  37699  dvreasin  37700  dvreacos  37701  areacirclem1  37702  dvrelog2  42052  dvrelog3  42053  aks6d1c2  42118  aks6d1c6lem3  42160  readvrec2  42349  readvrec  42350  resuppsinopn  42351  cantnf2  43314  limsupvaluz2  45736  supcnvlimsup  45738  itgperiod  45979  fourierdlem69  46173  fourierdlem73  46177  fourierdlem74  46178  fourierdlem75  46179  fourierdlem76  46180  fourierdlem81  46185  fourierdlem85  46189  fourierdlem88  46192  fourierdlem92  46196  fourierdlem97  46201  fourierdlem100  46204  fourierdlem101  46205  fourierdlem103  46207  fourierdlem104  46208  fourierdlem107  46211  fourierdlem111  46215  fourierdlem112  46216  fouriersw  46229  sge0tsms  46378  sge0resrnlem  46401  meadjiunlem  46463  omeunle  46514  isomenndlem  46528