Theorem fvmptd 6864

Description: Deduction version of fvmpt 6857. (Contributed by Scott Fenton, 18-Feb-2013.) (Revised by Mario Carneiro, 31-Aug-2015.) (Proof shortened by AV, 29-Mar-2024.)

Hypotheses

Ref	Expression
fvmptd.1	⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵))
fvmptd.2	⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶)
fvmptd.3	⊢ (𝜑 → 𝐴 ∈ 𝐷)
fvmptd.4	⊢ (𝜑 → 𝐶 ∈ 𝑉)

Assertion

Ref	Expression
fvmptd	⊢ (𝜑 → (𝐹‘𝐴) = 𝐶)

Distinct variable groups:   𝑥,𝐷   𝑥,𝐴   𝑥,𝐶   𝜑,𝑥

Allowed substitution hints:   𝐵(𝑥)   𝐹(𝑥)   𝑉(𝑥)

Proof of Theorem fvmptd

Step	Hyp	Ref	Expression
1		fvmptd.1	. 2 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵))
2		fvmptd.2	. 2 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝐵 = 𝐶)
3		fvmptd.3	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐷)
4		fvmptd.4	. 2 ⊢ (𝜑 → 𝐶 ∈ 𝑉)
5		nfv 1918	. 2 ⊢ Ⅎ𝑥𝜑
6		nfcv 2906	. 2 ⊢ Ⅎ𝑥𝐴
7		nfcv 2906	. 2 ⊢ Ⅎ𝑥𝐶
8	1, 2, 3, 4, 5, 6, 7	fvmptdf 6863	1 ⊢ (𝜑 → (𝐹‘𝐴) = 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2108   ↦ cmpt 5153  ‘cfv 6418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-iota 6376  df-fun 6420  df-fv 6426

This theorem is referenced by:  fvmptd2  6865  fvmptdv2  6875  fsplitfpar  7930  mpocurryvald  8057  fsetfocdm  8607  ttukeylem3  10198  ccatval1  14209  ccatval1OLD  14210  ccatval2  14211  repswsymb  14415  relexp1g  14665  rtrclreclem1  14696  rtrclreclem4  14700  dfrtrcl2  14701  prmodvdslcmf  16676  prmgap  16688  prmgaplcm  16689  prmgapprmo  16691  prdsvscafval  17108  mrcval  17236  cidval  17303  subcid  17478  idfu2nd  17508  resf2nd  17526  fuccoval  17597  fucid  17605  homaval  17662  idaval  17689  setcid  17717  catcid  17738  estrcid  17766  funcestrcsetclem1  17773  funcsetcestrclem1  17787  prf1  17833  prf2  17835  curf1  17859  curf11  17860  curf2val  17864  hof2  17891  yonedalem4a  17909  vrmdval  18411  smndex1gbas  18456  smndex1gid  18457  smndex1n0mnd  18466  mulgnngsum  18624  pj1val  19216  dpjval  19574  sraval  20353  frlmphl  20898  opsrval  21157  selvfval  21237  selvval  21238  mhpval  21240  mhpsclcl  21247  mhpmulcl  21249  cply1mul  21375  cply1coe0  21380  cply1coe0bi  21381  gsummoncoe1  21385  evls1sca  21399  mvmulfv  21601  mavmulfv  21603  mdetuni0  21678  mat2pmatval  21781  m2cpm  21798  cpm2mval  21807  m2cpminvid2lem  21811  decpmatid  21827  decpmatmullem  21828  pmatcollpw2lem  21834  monmatcollpw  21836  pm2mpfval  21853  mp2pm2mplem4  21866  pm2mpmhmlem2  21876  chpmatval  21888  fcfval  23092  cnextfval  23121  utopsnneiplem  23307  rrxmvallem  24473  rrxmval  24474  itgpowd  25119  taylpval  25431  lgamgulmlem2  26084  lgamcvglem  26094  logexprlim  26278  dchr1  26310  ishlg  26867  mirval  26920  mirfv  26921  ishpg  27024  lmif  27050  islmib  27052  lmodvslmhm  31212  psgnfzto1stlem  31269  tocycfv  31278  sgnsval  31330  madjusmdetlem2  31680  zarcls0  31720  zarcls1  31721  zarclsiin  31723  zarclsint  31724  zarclssn  31725  metidval  31742  pstmval  31747  qqhvval  31833  indval  31881  indfval  31884  esummulc1  31949  esumcvg  31954  ofcval  31967  sigagenval  32008  measinb  32089  omsfval  32161  omssubadd  32167  sitgfval  32208  eulerpartlemsv1  32223  eulerpartlems  32227  fibp1  32268  totprobd  32293  probmeasb  32297  dstrvprob  32338  dstfrvinc  32343  dstfrvclim1  32344  ballotlemfval  32356  ballotlemsv  32376  gsumnunsn  32420  signsply0  32430  signstfval  32443  fdvneggt  32480  fdvnegge  32482  itgexpif  32486  breprexplema  32510  vtsval  32517  logdivsqrle  32530  hgt750lemg  32534  afsval  32551  lpadval  32556  cvmliftlem9  33155  goel  33209  satf0suc  33238  sat1el2xp  33241  fmlafv  33242  fmla  33243  fmlasuc0  33246  ex-sategoelel  33283  ex-sategoelelomsuc  33288  mvrsval  33367  mrsubfval  33370  mrsubval  33371  msubfval  33386  msubval  33387  msrval  33400  fwddifval  34391  fwddifnval  34392  knoppcnlem1  34600  knoppcnlem4  34603  knoppcnlem6  34605  knoppcnlem7  34606  bj-imdirval2  35281  bj-iminvval2  35292  bj-fvmptunsn2  35356  bj-endval  35413  poimirlem1  35705  poimirlem2  35706  poimirlem5  35709  poimirlem6  35710  poimirlem7  35711  poimirlem10  35714  poimirlem11  35715  poimirlem12  35716  poimirlem19  35723  poimirlem22  35726  mblfinlem2  35742  areacirc  35797  tendopl2  38718  tendoi2  38736  erngplus2  38745  erngplus2-rN  38753  hlhilset  39875  lcmineqlem12  39976  aks4d1p9  40024  sticksstones2  40031  sticksstones3  40032  sticksstones6  40035  sticksstones7  40036  sticksstones8  40037  sticksstones10  40039  sticksstones12a  40041  sticksstones12  40042  sticksstones17  40047  sticksstones18  40048  sticksstones19  40049  metakunt3  40055  metakunt4  40056  metakunt5  40057  metakunt6  40058  metakunt7  40059  metakunt8  40060  metakunt10  40062  metakunt11  40063  metakunt12  40064  metakunt20  40072  metakunt21  40073  metakunt22  40074  metakunt26  40078  metakunt27  40079  metakunt28  40080  metakunt29  40081  metakunt30  40082  metakunt32  40084  fvmptd4  40136  rfovfvd  41499  rfovfvfvd  41500  rfovcnvf1od  41501  rfovcnvfvd  41504  fsovfvd  41507  fsovfvfvd  41508  fsovcnvlem  41510  dssmapfv2d  41515  dssmapfv3d  41516  dssmapnvod  41517  clsk3nimkb  41539  dvgrat  41819  radcnvrat  41821  hashnzfzclim  41829  binomcxplemnn0  41856  binomcxplemrat  41857  binomcxplemfrat  41858  binomcxplemradcnv  41859  binomcxplemcvg  41861  binomcxplemdvsum  41862  binomcxplemnotnn0  41863  mapss2  42634  fmuldfeqlem1  43013  clim1fr1  43032  climrec  43034  climexp  43036  climneg  43041  divcnvg  43058  sumnnodd  43061  supcnvlimsup  43171  icccncfext  43318  cncfioobdlem  43327  fprodsubrecnncnvlem  43338  fprodaddrecnncnvlem  43340  dvsinax  43344  fperdvper  43350  dvcosax  43357  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  dvnmul  43374  dvnprodlem1  43377  dvnprodlem2  43378  dvnprodlem3  43379  itgsinexp  43386  itgcoscmulx  43400  itgsincmulx  43405  itgsubsticclem  43406  itgsubsticc  43407  itgiccshift  43411  wallispilem5  43500  wallispi  43501  wallispi2lem1  43502  wallispi2lem2  43503  wallispi2  43504  stirlinglem1  43505  stirlinglem2  43506  stirlinglem3  43507  stirlinglem4  43508  stirlinglem5  43509  stirlinglem7  43511  stirlinglem8  43512  stirlinglem10  43514  stirlinglem11  43515  stirlinglem12  43516  stirlinglem13  43517  stirlinglem14  43518  stirlinglem15  43519  dirkerval2  43525  dirkercncflem2  43535  fourierdlem7  43545  fourierdlem13  43551  fourierdlem14  43552  fourierdlem16  43554  fourierdlem18  43556  fourierdlem19  43557  fourierdlem21  43559  fourierdlem22  43560  fourierdlem26  43564  fourierdlem37  43575  fourierdlem39  43577  fourierdlem41  43579  fourierdlem48  43585  fourierdlem49  43586  fourierdlem50  43587  fourierdlem51  43588  fourierdlem53  43590  fourierdlem62  43599  fourierdlem63  43600  fourierdlem65  43602  fourierdlem73  43610  fourierdlem74  43611  fourierdlem75  43612  fourierdlem76  43613  fourierdlem79  43616  fourierdlem81  43618  fourierdlem82  43619  fourierdlem83  43620  fourierdlem84  43621  fourierdlem88  43625  fourierdlem89  43626  fourierdlem90  43627  fourierdlem91  43628  fourierdlem92  43629  fourierdlem93  43630  fourierdlem97  43634  fourierdlem101  43638  fourierdlem103  43640  fourierdlem104  43641  fourierdlem111  43648  fourierdlem112  43649  fouriersw  43662  elaa2lem  43664  etransclem13  43678  etransclem17  43682  etransclem18  43683  etransclem21  43686  etransclem31  43696  etransclem32  43697  etransclem33  43698  etransclem35  43700  etransclem46  43711  etransclem48  43713  rrxtopnfi  43718  salgenval  43752  sge0val  43794  sge0z  43803  sge0snmpt  43811  sge0xp  43857  nnfoctbdjlem  43883  omeiunltfirp  43947  caratheodorylem1  43954  0ome  43957  ovnval2  43973  hoicvr  43976  ovncvrrp  43992  ovn0lem  43993  ovnsubaddlem1  43998  hsphoif  44004  hsphoival  44007  hoidmv1le  44022  hoidmvlelem3  44025  ovnhoilem2  44030  ovncvr2  44039  hoidifhspval2  44043  hoidifhspval3  44047  hspmbllem2  44055  smfid  44175  fsetsnf1  44433  fsetsnfo  44434  cfsetsnfsetfv  44438  cfsetsnfsetfo  44441  fvmptrab  44671  fundcmpsurinjlem3  44740  sprval  44819  prproropreud  44849  isomuspgrlem2a  45168  c0mgm  45355  c0mhm  45356  c0snmgmhm  45360  c0snmhm  45361  zrrnghm  45363  rngcvalALTV  45407  rngcidALTV  45437  zrinitorngc  45446  zrtermorngc  45447  ringcvalALTV  45453  funcringcsetcALTV2lem1  45482  ringcidALTV  45500  funcringcsetclem1ALTV  45505  zrtermoringc  45516  rhmsubcALTVlem3  45552  scmsuppss  45596  ply1mulgsum  45619  lindslinindsimp1  45686  lindsrng01  45697  islindeps2  45712  fdivmptfv  45779  refdivmptfv  45780  1arympt1fv  45873  itcoval0  45896  itcoval1  45897  itcoval2  45898  itcoval3  45899  itcovalsuc  45901  ackvalsuc1mpt  45912  ackvalsuc1  45913  ackval1  45915  ackval2  45916  ackval3  45917  ackval0val  45920  mndtcid  46262  amgmwlem  46392