Theorem fvmptd 6955

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114   ↦ cmpt 5166  ‘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-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-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  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-iota 6454  df-fun 6500  df-fv 6506

This theorem is referenced by:  fvmptd2  6956  fvmptdv2  6966  fvmptd4  6972  mptcnfimad  7939  fsplitfpar  8068  mpocurryvald  8220  ttukeylem3  10433  indval  12162  indfval  12166  tpf1ofv0  14458  tpf1ofv1  14459  tpf1ofv2  14460  ccatval1  14539  ccatval2  14540  repswsymb  14736  relexp1g  14988  rtrclreclem1  15019  rtrclreclem4  15023  dfrtrcl2  15024  prmodvdslcmf  17018  prmgap  17030  prmgaplcm  17031  prmgapprmo  17033  prdsvscafval  17443  mrcval  17576  cidval  17643  subcid  17814  idfu2nd  17844  resf2nd  17862  fuccoval  17933  fucid  17941  homaval  17998  idaval  18025  setcid  18053  catcid  18074  estrcid  18100  funcestrcsetclem1  18106  funcsetcestrclem1  18120  prf1  18166  prf2  18168  curf1  18191  curf11  18192  curf2val  18196  hof2  18223  yonedalem4a  18241  vrmdval  18825  smndex1gbasOLD  18871  smndex1gid  18872  smndex1gidOLD  18873  smndex1n0mnd  18883  mulgnngsum  19055  pj1val  19670  dpjval  20033  c0mgm  20439  c0mhm  20440  c0snmgmhm  20442  c0snmhm  20443  zrrnghm  20513  zrinitorngc  20619  zrtermorngc  20620  zrtermoringc  20652  sraval  21170  rngqiprngimfv  21296  frlmphl  21761  opsrval  22024  selvfval  22100  mhpval  22105  mhpsclcl  22113  psdfval  22124  cply1mul  22261  cply1coe0  22266  cply1coe0bi  22267  gsummoncoe1  22273  evls1sca  22288  mvmulfv  22509  mavmulfv  22511  mdetuni0  22586  mat2pmatval  22689  m2cpm  22706  cpm2mval  22715  m2cpminvid2lem  22719  decpmatid  22735  decpmatmullem  22736  pmatcollpw2lem  22742  monmatcollpw  22744  pm2mpfval  22761  mp2pm2mplem4  22774  pm2mpmhmlem2  22784  chpmatval  22796  fcfval  23998  cnextfval  24027  utopsnneiplem  24212  rrxmvallem  25371  rrxmval  25372  itgpowd  26017  taylpval  26332  lgamgulmlem2  26993  lgamcvglem  27003  logexprlim  27188  dchr1  27220  ishlg  28670  mirval  28723  mirfv  28724  ishpg  28827  lmif  28853  islmib  28855  lmodvslmhm  33111  psgnfzto1stlem  33161  tocycfv  33170  sgnsval  33222  mplvrpmrhm  33691  esplyfval0  33708  esplyind  33719  evls1fldgencl  33814  minplyval  33849  rtelextdg2lem  33870  2sqr3minply  33924  cos9thpiminply  33932  zarcls0  34012  zarcls1  34013  zarclsiin  34015  zarclsint  34016  zarclssn  34017  qqhvval  34127  esummulc1  34225  esumcvg  34230  ofcval  34243  sigagenval  34284  measinb  34365  omsfval  34438  omssubadd  34444  sitgfval  34485  eulerpartlemsv1  34500  eulerpartlems  34504  fibp1  34545  totprobd  34570  probmeasb  34574  dstrvprob  34616  dstfrvinc  34621  dstfrvclim1  34622  ballotlemfval  34634  ballotlemsv  34654  gsumnunsn  34685  signsply0  34695  signstfval  34708  fdvneggt  34744  fdvnegge  34746  itgexpif  34750  breprexplema  34774  vtsval  34781  logdivsqrle  34794  hgt750lemg  34798  afsval  34815  lpadval  34820  cvmliftlem9  35475  goel  35529  satf0suc  35558  sat1el2xp  35561  fmlafv  35562  fmla  35563  fmlasuc0  35566  ex-sategoelel  35603  ex-sategoelelomsuc  35608  mvrsval  35687  mrsubfval  35690  mrsubval  35691  msubfval  35706  msubval  35707  msrval  35720  fwddifval  36344  fwddifnval  36345  knoppcnlem1  36753  knoppcnlem4  36756  knoppcnlem6  36758  knoppcnlem7  36759  bj-imdirval2  37497  bj-iminvval2  37508  bj-fvmptunsn2  37572  bj-endval  37629  poimirlem1  37942  poimirlem2  37943  poimirlem5  37946  poimirlem6  37947  poimirlem7  37948  poimirlem10  37951  poimirlem11  37952  poimirlem12  37953  poimirlem19  37960  poimirlem22  37963  mblfinlem2  37979  areacirc  38034  tendopl2  41223  tendoi2  41241  erngplus2  41250  erngplus2-rN  41258  hlhilset  42380  rhmzrhval  42411  lcmineqlem12  42479  aks4d1p9  42527  primrootscoprbij  42541  aks6d1c1p3  42549  aks6d1c1p5  42551  aks6d1c1  42555  hashscontpow  42561  aks6d1c3  42562  aks6d1c4  42563  aks6d1c2lem4  42566  aks6d1c2  42569  aks6d1c5lem3  42576  deg1gprod  42579  sticksstones2  42586  sticksstones3  42587  sticksstones6  42590  sticksstones7  42591  sticksstones8  42592  sticksstones10  42594  sticksstones12a  42596  sticksstones12  42597  sticksstones17  42602  sticksstones18  42603  sticksstones19  42604  aks6d1c6lem1  42609  aks6d1c6lem2  42610  aks6d1c6lem3  42611  aks6d1c6lem4  42612  aks6d1c6isolem1  42613  aks6d1c6isolem2  42614  aks6d1c6isolem3  42615  aks6d1c6lem5  42616  aks6d1c7lem1  42619  aks5lem2  42626  aks5lem3a  42628  unitscyglem1  42634  rfovfvd  44429  rfovfvfvd  44430  rfovcnvf1od  44431  rfovcnvfvd  44434  fsovfvd  44437  fsovfvfvd  44438  fsovcnvlem  44440  dssmapfv2d  44445  dssmapfv3d  44446  dssmapnvod  44447  clsk3nimkb  44467  dvgrat  44739  radcnvrat  44741  hashnzfzclim  44749  binomcxplemnn0  44776  binomcxplemrat  44777  binomcxplemfrat  44778  binomcxplemradcnv  44779  binomcxplemcvg  44781  binomcxplemdvsum  44782  binomcxplemnotnn0  44783  mapss2  45634  fmuldfeqlem1  46012  clim1fr1  46031  climrec  46033  climexp  46035  climneg  46040  divcnvg  46057  sumnnodd  46060  supcnvlimsup  46168  icccncfext  46315  cncfioobdlem  46324  fprodsubrecnncnvlem  46335  fprodaddrecnncnvlem  46337  dvsinax  46341  fperdvper  46347  dvcosax  46354  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  dvnmul  46371  dvnprodlem1  46374  dvnprodlem2  46375  dvnprodlem3  46376  itgsinexp  46383  itgcoscmulx  46397  itgsincmulx  46402  itgsubsticclem  46403  itgsubsticc  46404  itgiccshift  46408  wallispilem5  46497  wallispi  46498  wallispi2lem1  46499  wallispi2lem2  46500  wallispi2  46501  stirlinglem1  46502  stirlinglem2  46503  stirlinglem3  46504  stirlinglem4  46505  stirlinglem5  46506  stirlinglem7  46508  stirlinglem8  46509  stirlinglem10  46511  stirlinglem11  46512  stirlinglem12  46513  stirlinglem13  46514  stirlinglem14  46515  stirlinglem15  46516  dirkerval2  46522  dirkercncflem2  46532  fourierdlem7  46542  fourierdlem13  46548  fourierdlem14  46549  fourierdlem16  46551  fourierdlem18  46553  fourierdlem19  46554  fourierdlem21  46556  fourierdlem22  46557  fourierdlem26  46561  fourierdlem37  46572  fourierdlem39  46574  fourierdlem41  46576  fourierdlem48  46582  fourierdlem49  46583  fourierdlem50  46584  fourierdlem51  46585  fourierdlem53  46587  fourierdlem62  46596  fourierdlem63  46597  fourierdlem65  46599  fourierdlem73  46607  fourierdlem74  46608  fourierdlem75  46609  fourierdlem76  46610  fourierdlem79  46613  fourierdlem81  46615  fourierdlem82  46616  fourierdlem83  46617  fourierdlem84  46618  fourierdlem88  46622  fourierdlem89  46623  fourierdlem90  46624  fourierdlem91  46625  fourierdlem92  46626  fourierdlem93  46627  fourierdlem97  46631  fourierdlem101  46635  fourierdlem103  46637  fourierdlem104  46638  fourierdlem111  46645  fourierdlem112  46646  fouriersw  46659  elaa2lem  46661  etransclem13  46675  etransclem17  46679  etransclem18  46680  etransclem21  46683  etransclem31  46693  etransclem32  46694  etransclem33  46695  etransclem35  46697  etransclem46  46708  etransclem48  46710  rrxtopnfi  46715  salgenval  46749  sge0val  46794  sge0z  46803  sge0snmpt  46811  sge0xp  46857  nnfoctbdjlem  46883  omeiunltfirp  46947  caratheodorylem1  46954  0ome  46957  ovnval2  46973  hoicvr  46976  ovncvrrp  46992  ovn0lem  46993  ovnsubaddlem1  46998  hsphoif  47004  hsphoival  47007  hoidmv1le  47022  hoidmvlelem3  47025  ovnhoilem2  47030  ovncvr2  47039  hoidifhspval2  47043  hoidifhspval3  47047  hspmbllem2  47055  smfid  47180  fsetsnf1  47500  fsetsnfo  47501  cfsetsnfsetfv  47505  cfsetsnfsetfo  47508  fvmptrab  47740  fundcmpsurinjlem3  47860  sprval  47939  prproropreud  47969  upgrimwlklem3  48375  grtri  48416  stgrfv  48429  isubgr3stgrlem5  48446  rngcvalALTV  48741  rngcidALTV  48750  rhmsubcALTVlem3  48759  ringcvalALTV  48765  funcringcsetcALTV2lem1  48766  ringcidALTV  48784  funcringcsetclem1ALTV  48789  scmsuppss  48847  ply1mulgsum  48866  lindslinindsimp1  48933  lindsrng01  48944  islindeps2  48959  fdivmptfv  49021  refdivmptfv  49022  1arympt1fv  49115  itcoval0  49138  itcoval1  49139  itcoval2  49140  itcoval3  49141  itcovalsuc  49143  ackvalsuc1mpt  49154  ackvalsuc1  49155  ackval1  49157  ackval2  49158  ackval3  49159  ackval0val  49162  swapf1a  49744  swapf2a  49746  swapf1  49747  swapf2  49749  tposcurf2val  49776  fuco23  49816  prcof1  49863  prcof21a  49866  mndtcid  50064  amgmwlem  50277