MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  feqresmpt Structured version   Visualization version   GIF version

Theorem feqresmpt 6916
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
StepHypRef Expression
1 feqmptd.1 . . . 4 (𝜑𝐹:𝐴𝐵)
2 feqresmpt.2 . . . 4 (𝜑𝐶𝐴)
31, 2fssresd 6714 . . 3 (𝜑 → (𝐹𝐶):𝐶𝐵)
43feqmptd 6915 . 2 (𝜑 → (𝐹𝐶) = (𝑥𝐶 ↦ ((𝐹𝐶)‘𝑥)))
5 fvres 6866 . . 3 (𝑥𝐶 → ((𝐹𝐶)‘𝑥) = (𝐹𝑥))
65mpteq2ia 5213 . 2 (𝑥𝐶 ↦ ((𝐹𝐶)‘𝑥)) = (𝑥𝐶 ↦ (𝐹𝑥))
74, 6eqtrdi 2793 1 (𝜑 → (𝐹𝐶) = (𝑥𝐶 ↦ (𝐹𝑥)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wss 3915  cmpt 5193  cres 5640  wf 6497  cfv 6501
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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5261  ax-nul 5268  ax-pr 5389
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-rab 3411  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-fv 6509
This theorem is referenced by:  pwfseqlem5  10606  pfxres  14574  gsumpt  19746  dpjidcl  19844  regsumsupp  21042  tsmsxplem2  23521  dvmulbr  25319  dvlip  25373  lhop1lem  25393  loglesqrt  26127  jensenlem1  26352  jensen  26354  amgm  26356  ushgredgedg  28219  ushgredgedgloop  28221  mgcf1o  31905  gsumzresunsn  31938  gsumpart  31939  gsumhashmul  31940  gsumle  31974  coinflippv  33123  fdvposlt  33252  fdvposle  33254  logdivsqrle  33303  ftc1cnnclem  36178  dvasin  36191  dvacos  36192  dvreasin  36193  dvreacos  36194  areacirclem1  36195  dvrelog2  40550  dvrelog3  40551  cantnf2  41689  limsupvaluz2  44053  supcnvlimsup  44055  itgperiod  44296  fourierdlem69  44490  fourierdlem73  44494  fourierdlem74  44495  fourierdlem75  44496  fourierdlem76  44497  fourierdlem81  44502  fourierdlem85  44506  fourierdlem88  44509  fourierdlem92  44513  fourierdlem97  44518  fourierdlem100  44521  fourierdlem101  44522  fourierdlem103  44524  fourierdlem104  44525  fourierdlem107  44528  fourierdlem111  44532  fourierdlem112  44533  fouriersw  44546  sge0tsms  44695  sge0resrnlem  44718  meadjiunlem  44780  omeunle  44831  isomenndlem  44845
  Copyright terms: Public domain W3C validator