Theorem fvmptd 6891

Description: Deduction version of fvmpt 6884. (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 2908	. 2 ⊢ Ⅎ𝑥𝐴
7		nfcv 2908	. 2 ⊢ Ⅎ𝑥𝐶
8	1, 2, 3, 4, 5, 6, 7	fvmptdf 6890	1 ⊢ (𝜑 → (𝐹‘𝐴) = 𝐶)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ∈ wcel 2107   ↦ cmpt 5158  ‘cfv 6437

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 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-iota 6395  df-fun 6439  df-fv 6445

This theorem is referenced by:  fvmptd2  6892  fvmptdv2  6902  fsplitfpar  7968  mpocurryvald  8095  fsetfocdm  8658  ttukeylem3  10276  ccatval1  14290  ccatval1OLD  14291  ccatval2  14292  repswsymb  14496  relexp1g  14746  rtrclreclem1  14777  rtrclreclem4  14781  dfrtrcl2  14782  prmodvdslcmf  16757  prmgap  16769  prmgaplcm  16770  prmgapprmo  16772  prdsvscafval  17200  mrcval  17328  cidval  17395  subcid  17571  idfu2nd  17601  resf2nd  17619  fuccoval  17690  fucid  17698  homaval  17755  idaval  17782  setcid  17810  catcid  17831  estrcid  17859  funcestrcsetclem1  17866  funcsetcestrclem1  17880  prf1  17926  prf2  17928  curf1  17952  curf11  17953  curf2val  17957  hof2  17984  yonedalem4a  18002  vrmdval  18505  smndex1gbas  18550  smndex1gid  18551  smndex1n0mnd  18560  mulgnngsum  18718  pj1val  19310  dpjval  19668  sraval  20447  frlmphl  20997  opsrval  21256  selvfval  21336  selvval  21337  mhpval  21339  mhpsclcl  21346  mhpmulcl  21348  cply1mul  21474  cply1coe0  21479  cply1coe0bi  21480  gsummoncoe1  21484  evls1sca  21498  mvmulfv  21702  mavmulfv  21704  mdetuni0  21779  mat2pmatval  21882  m2cpm  21899  cpm2mval  21908  m2cpminvid2lem  21912  decpmatid  21928  decpmatmullem  21929  pmatcollpw2lem  21935  monmatcollpw  21937  pm2mpfval  21954  mp2pm2mplem4  21967  pm2mpmhmlem2  21977  chpmatval  21989  fcfval  23193  cnextfval  23222  utopsnneiplem  23408  rrxmvallem  24577  rrxmval  24578  itgpowd  25223  taylpval  25535  lgamgulmlem2  26188  lgamcvglem  26198  logexprlim  26382  dchr1  26414  ishlg  26972  mirval  27025  mirfv  27026  ishpg  27129  lmif  27155  islmib  27157  lmodvslmhm  31319  psgnfzto1stlem  31376  tocycfv  31385  sgnsval  31437  madjusmdetlem2  31787  zarcls0  31827  zarcls1  31828  zarclsiin  31830  zarclsint  31831  zarclssn  31832  metidval  31849  pstmval  31854  qqhvval  31942  indval  31990  indfval  31993  esummulc1  32058  esumcvg  32063  ofcval  32076  sigagenval  32117  measinb  32198  omsfval  32270  omssubadd  32276  sitgfval  32317  eulerpartlemsv1  32332  eulerpartlems  32336  fibp1  32377  totprobd  32402  probmeasb  32406  dstrvprob  32447  dstfrvinc  32452  dstfrvclim1  32453  ballotlemfval  32465  ballotlemsv  32485  gsumnunsn  32529  signsply0  32539  signstfval  32552  fdvneggt  32589  fdvnegge  32591  itgexpif  32595  breprexplema  32619  vtsval  32626  logdivsqrle  32639  hgt750lemg  32643  afsval  32660  lpadval  32665  cvmliftlem9  33264  goel  33318  satf0suc  33347  sat1el2xp  33350  fmlafv  33351  fmla  33352  fmlasuc0  33355  ex-sategoelel  33392  ex-sategoelelomsuc  33397  mvrsval  33476  mrsubfval  33479  mrsubval  33480  msubfval  33495  msubval  33496  msrval  33509  fwddifval  34473  fwddifnval  34474  knoppcnlem1  34682  knoppcnlem4  34685  knoppcnlem6  34687  knoppcnlem7  34688  bj-imdirval2  35363  bj-iminvval2  35374  bj-fvmptunsn2  35438  bj-endval  35495  poimirlem1  35787  poimirlem2  35788  poimirlem5  35791  poimirlem6  35792  poimirlem7  35793  poimirlem10  35796  poimirlem11  35797  poimirlem12  35798  poimirlem19  35805  poimirlem22  35808  mblfinlem2  35824  areacirc  35879  tendopl2  38798  tendoi2  38816  erngplus2  38825  erngplus2-rN  38833  hlhilset  39955  lcmineqlem12  40055  aks4d1p9  40103  sticksstones2  40110  sticksstones3  40111  sticksstones6  40114  sticksstones7  40115  sticksstones8  40116  sticksstones10  40118  sticksstones12a  40120  sticksstones12  40121  sticksstones17  40126  sticksstones18  40127  sticksstones19  40128  metakunt3  40134  metakunt4  40135  metakunt5  40136  metakunt6  40137  metakunt7  40138  metakunt8  40139  metakunt10  40141  metakunt11  40142  metakunt12  40143  metakunt20  40151  metakunt21  40152  metakunt22  40153  metakunt26  40157  metakunt27  40158  metakunt28  40159  metakunt29  40160  metakunt30  40161  metakunt32  40163  fvmptd4  40217  rfovfvd  41617  rfovfvfvd  41618  rfovcnvf1od  41619  rfovcnvfvd  41622  fsovfvd  41625  fsovfvfvd  41626  fsovcnvlem  41628  dssmapfv2d  41633  dssmapfv3d  41634  dssmapnvod  41635  clsk3nimkb  41657  dvgrat  41937  radcnvrat  41939  hashnzfzclim  41947  binomcxplemnn0  41974  binomcxplemrat  41975  binomcxplemfrat  41976  binomcxplemradcnv  41977  binomcxplemcvg  41979  binomcxplemdvsum  41980  binomcxplemnotnn0  41981  mapss2  42752  fmuldfeqlem1  43130  clim1fr1  43149  climrec  43151  climexp  43153  climneg  43158  divcnvg  43175  sumnnodd  43178  supcnvlimsup  43288  icccncfext  43435  cncfioobdlem  43444  fprodsubrecnncnvlem  43455  fprodaddrecnncnvlem  43457  dvsinax  43461  fperdvper  43467  dvcosax  43474  ioodvbdlimc1lem2  43480  ioodvbdlimc2lem  43482  dvnmul  43491  dvnprodlem1  43494  dvnprodlem2  43495  dvnprodlem3  43496  itgsinexp  43503  itgcoscmulx  43517  itgsincmulx  43522  itgsubsticclem  43523  itgsubsticc  43524  itgiccshift  43528  wallispilem5  43617  wallispi  43618  wallispi2lem1  43619  wallispi2lem2  43620  wallispi2  43621  stirlinglem1  43622  stirlinglem2  43623  stirlinglem3  43624  stirlinglem4  43625  stirlinglem5  43626  stirlinglem7  43628  stirlinglem8  43629  stirlinglem10  43631  stirlinglem11  43632  stirlinglem12  43633  stirlinglem13  43634  stirlinglem14  43635  stirlinglem15  43636  dirkerval2  43642  dirkercncflem2  43652  fourierdlem7  43662  fourierdlem13  43668  fourierdlem14  43669  fourierdlem16  43671  fourierdlem18  43673  fourierdlem19  43674  fourierdlem21  43676  fourierdlem22  43677  fourierdlem26  43681  fourierdlem37  43692  fourierdlem39  43694  fourierdlem41  43696  fourierdlem48  43702  fourierdlem49  43703  fourierdlem50  43704  fourierdlem51  43705  fourierdlem53  43707  fourierdlem62  43716  fourierdlem63  43717  fourierdlem65  43719  fourierdlem73  43727  fourierdlem74  43728  fourierdlem75  43729  fourierdlem76  43730  fourierdlem79  43733  fourierdlem81  43735  fourierdlem82  43736  fourierdlem83  43737  fourierdlem84  43738  fourierdlem88  43742  fourierdlem89  43743  fourierdlem90  43744  fourierdlem91  43745  fourierdlem92  43746  fourierdlem93  43747  fourierdlem97  43751  fourierdlem101  43755  fourierdlem103  43757  fourierdlem104  43758  fourierdlem111  43765  fourierdlem112  43766  fouriersw  43779  elaa2lem  43781  etransclem13  43795  etransclem17  43799  etransclem18  43800  etransclem21  43803  etransclem31  43813  etransclem32  43814  etransclem33  43815  etransclem35  43817  etransclem46  43828  etransclem48  43830  rrxtopnfi  43835  salgenval  43869  sge0val  43911  sge0z  43920  sge0snmpt  43928  sge0xp  43974  nnfoctbdjlem  44000  omeiunltfirp  44064  caratheodorylem1  44071  0ome  44074  ovnval2  44090  hoicvr  44093  ovncvrrp  44109  ovn0lem  44110  ovnsubaddlem1  44115  hsphoif  44121  hsphoival  44124  hoidmv1le  44139  hoidmvlelem3  44142  ovnhoilem2  44147  ovncvr2  44156  hoidifhspval2  44160  hoidifhspval3  44164  hspmbllem2  44172  smfid  44297  fsetsnf1  44557  fsetsnfo  44558  cfsetsnfsetfv  44562  cfsetsnfsetfo  44565  fvmptrab  44795  fundcmpsurinjlem3  44863  sprval  44942  prproropreud  44972  isomuspgrlem2a  45291  c0mgm  45478  c0mhm  45479  c0snmgmhm  45483  c0snmhm  45484  zrrnghm  45486  rngcvalALTV  45530  rngcidALTV  45560  zrinitorngc  45569  zrtermorngc  45570  ringcvalALTV  45576  funcringcsetcALTV2lem1  45605  ringcidALTV  45623  funcringcsetclem1ALTV  45628  zrtermoringc  45639  rhmsubcALTVlem3  45675  scmsuppss  45719  ply1mulgsum  45742  lindslinindsimp1  45809  lindsrng01  45820  islindeps2  45835  fdivmptfv  45902  refdivmptfv  45903  1arympt1fv  45996  itcoval0  46019  itcoval1  46020  itcoval2  46021  itcoval3  46022  itcovalsuc  46024  ackvalsuc1mpt  46035  ackvalsuc1  46036  ackval1  46038  ackval2  46039  ackval3  46040  ackval0val  46043  mndtcid  46387  amgmwlem  46517