Theorem fvmptd 6944

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113   ↦ cmpt 5176  ‘cfv 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-iota 6444  df-fun 6490  df-fv 6496

This theorem is referenced by:  fvmptd2  6945  fvmptdv2  6955  fvmptd4  6961  mptcnfimad  7926  fsplitfpar  8056  mpocurryvald  8208  ttukeylem3  10411  tpf1ofv0  14407  tpf1ofv1  14408  tpf1ofv2  14409  ccatval1  14488  ccatval2  14489  repswsymb  14685  relexp1g  14937  rtrclreclem1  14968  rtrclreclem4  14972  dfrtrcl2  14973  prmodvdslcmf  16963  prmgap  16975  prmgaplcm  16976  prmgapprmo  16978  prdsvscafval  17388  mrcval  17520  cidval  17587  subcid  17758  idfu2nd  17788  resf2nd  17806  fuccoval  17877  fucid  17885  homaval  17942  idaval  17969  setcid  17997  catcid  18018  estrcid  18044  funcestrcsetclem1  18050  funcsetcestrclem1  18064  prf1  18110  prf2  18112  curf1  18135  curf11  18136  curf2val  18140  hof2  18167  yonedalem4a  18185  vrmdval  18769  smndex1gbas  18814  smndex1gid  18815  smndex1n0mnd  18824  mulgnngsum  18996  pj1val  19611  dpjval  19974  c0mgm  20381  c0mhm  20382  c0snmgmhm  20384  c0snmhm  20385  zrrnghm  20455  zrinitorngc  20561  zrtermorngc  20562  zrtermoringc  20594  sraval  21113  rngqiprngimfv  21239  frlmphl  21722  opsrval  21984  selvfval  22052  mhpval  22057  mhpsclcl  22065  psdfval  22076  cply1mul  22214  cply1coe0  22219  cply1coe0bi  22220  gsummoncoe1  22226  evls1sca  22241  mvmulfv  22462  mavmulfv  22464  mdetuni0  22539  mat2pmatval  22642  m2cpm  22659  cpm2mval  22668  m2cpminvid2lem  22672  decpmatid  22688  decpmatmullem  22689  pmatcollpw2lem  22695  monmatcollpw  22697  pm2mpfval  22714  mp2pm2mplem4  22727  pm2mpmhmlem2  22737  chpmatval  22749  fcfval  23951  cnextfval  23980  utopsnneiplem  24165  rrxmvallem  25334  rrxmval  25335  itgpowd  25987  taylpval  26304  lgamgulmlem2  26970  lgamcvglem  26980  logexprlim  27166  dchr1  27198  ishlg  28583  mirval  28636  mirfv  28637  ishpg  28740  lmif  28766  islmib  28768  indval  32841  indfval  32844  lmodvslmhm  33039  psgnfzto1stlem  33078  tocycfv  33087  sgnsval  33139  mplvrpmrhm  33597  esplyind  33615  evls1fldgencl  33706  minplyval  33741  rtelextdg2lem  33762  2sqr3minply  33816  cos9thpiminply  33824  zarcls0  33904  zarcls1  33905  zarclsiin  33907  zarclsint  33908  zarclssn  33909  qqhvval  34019  esummulc1  34117  esumcvg  34122  ofcval  34135  sigagenval  34176  measinb  34257  omsfval  34330  omssubadd  34336  sitgfval  34377  eulerpartlemsv1  34392  eulerpartlems  34396  fibp1  34437  totprobd  34462  probmeasb  34466  dstrvprob  34508  dstfrvinc  34513  dstfrvclim1  34514  ballotlemfval  34526  ballotlemsv  34546  gsumnunsn  34577  signsply0  34587  signstfval  34600  fdvneggt  34636  fdvnegge  34638  itgexpif  34642  breprexplema  34666  vtsval  34673  logdivsqrle  34686  hgt750lemg  34690  afsval  34707  lpadval  34712  cvmliftlem9  35360  goel  35414  satf0suc  35443  sat1el2xp  35446  fmlafv  35447  fmla  35448  fmlasuc0  35451  ex-sategoelel  35488  ex-sategoelelomsuc  35493  mvrsval  35572  mrsubfval  35575  mrsubval  35576  msubfval  35591  msubval  35592  msrval  35605  fwddifval  36229  fwddifnval  36230  knoppcnlem1  36560  knoppcnlem4  36563  knoppcnlem6  36565  knoppcnlem7  36566  bj-imdirval2  37250  bj-iminvval2  37261  bj-fvmptunsn2  37325  bj-endval  37382  poimirlem1  37684  poimirlem2  37685  poimirlem5  37688  poimirlem6  37689  poimirlem7  37690  poimirlem10  37693  poimirlem11  37694  poimirlem12  37695  poimirlem19  37702  poimirlem22  37705  mblfinlem2  37721  areacirc  37776  tendopl2  40899  tendoi2  40917  erngplus2  40926  erngplus2-rN  40934  hlhilset  42056  rhmzrhval  42087  lcmineqlem12  42156  aks4d1p9  42204  primrootscoprbij  42218  aks6d1c1p3  42226  aks6d1c1p5  42228  aks6d1c1  42232  hashscontpow  42238  aks6d1c3  42239  aks6d1c4  42240  aks6d1c2lem4  42243  aks6d1c2  42246  aks6d1c5lem3  42253  deg1gprod  42256  sticksstones2  42263  sticksstones3  42264  sticksstones6  42267  sticksstones7  42268  sticksstones8  42269  sticksstones10  42271  sticksstones12a  42273  sticksstones12  42274  sticksstones17  42279  sticksstones18  42280  sticksstones19  42281  aks6d1c6lem1  42286  aks6d1c6lem2  42287  aks6d1c6lem3  42288  aks6d1c6lem4  42289  aks6d1c6isolem1  42290  aks6d1c6isolem2  42291  aks6d1c6isolem3  42292  aks6d1c6lem5  42293  aks6d1c7lem1  42296  aks5lem2  42303  aks5lem3a  42305  unitscyglem1  42311  rfovfvd  44122  rfovfvfvd  44123  rfovcnvf1od  44124  rfovcnvfvd  44127  fsovfvd  44130  fsovfvfvd  44131  fsovcnvlem  44133  dssmapfv2d  44138  dssmapfv3d  44139  dssmapnvod  44140  clsk3nimkb  44160  dvgrat  44432  radcnvrat  44434  hashnzfzclim  44442  binomcxplemnn0  44469  binomcxplemrat  44470  binomcxplemfrat  44471  binomcxplemradcnv  44472  binomcxplemcvg  44474  binomcxplemdvsum  44475  binomcxplemnotnn0  44476  mapss2  45329  fmuldfeqlem1  45709  clim1fr1  45728  climrec  45730  climexp  45732  climneg  45737  divcnvg  45754  sumnnodd  45757  supcnvlimsup  45865  icccncfext  46012  cncfioobdlem  46021  fprodsubrecnncnvlem  46032  fprodaddrecnncnvlem  46034  dvsinax  46038  fperdvper  46044  dvcosax  46051  ioodvbdlimc1lem2  46057  ioodvbdlimc2lem  46059  dvnmul  46068  dvnprodlem1  46071  dvnprodlem2  46072  dvnprodlem3  46073  itgsinexp  46080  itgcoscmulx  46094  itgsincmulx  46099  itgsubsticclem  46100  itgsubsticc  46101  itgiccshift  46105  wallispilem5  46194  wallispi  46195  wallispi2lem1  46196  wallispi2lem2  46197  wallispi2  46198  stirlinglem1  46199  stirlinglem2  46200  stirlinglem3  46201  stirlinglem4  46202  stirlinglem5  46203  stirlinglem7  46205  stirlinglem8  46206  stirlinglem10  46208  stirlinglem11  46209  stirlinglem12  46210  stirlinglem13  46211  stirlinglem14  46212  stirlinglem15  46213  dirkerval2  46219  dirkercncflem2  46229  fourierdlem7  46239  fourierdlem13  46245  fourierdlem14  46246  fourierdlem16  46248  fourierdlem18  46250  fourierdlem19  46251  fourierdlem21  46253  fourierdlem22  46254  fourierdlem26  46258  fourierdlem37  46269  fourierdlem39  46271  fourierdlem41  46273  fourierdlem48  46279  fourierdlem49  46280  fourierdlem50  46281  fourierdlem51  46282  fourierdlem53  46284  fourierdlem62  46293  fourierdlem63  46294  fourierdlem65  46296  fourierdlem73  46304  fourierdlem74  46305  fourierdlem75  46306  fourierdlem76  46307  fourierdlem79  46310  fourierdlem81  46312  fourierdlem82  46313  fourierdlem83  46314  fourierdlem84  46315  fourierdlem88  46319  fourierdlem89  46320  fourierdlem90  46321  fourierdlem91  46322  fourierdlem92  46323  fourierdlem93  46324  fourierdlem97  46328  fourierdlem101  46332  fourierdlem103  46334  fourierdlem104  46335  fourierdlem111  46342  fourierdlem112  46343  fouriersw  46356  elaa2lem  46358  etransclem13  46372  etransclem17  46376  etransclem18  46377  etransclem21  46380  etransclem31  46390  etransclem32  46391  etransclem33  46392  etransclem35  46394  etransclem46  46405  etransclem48  46407  rrxtopnfi  46412  salgenval  46446  sge0val  46491  sge0z  46500  sge0snmpt  46508  sge0xp  46554  nnfoctbdjlem  46580  omeiunltfirp  46644  caratheodorylem1  46651  0ome  46654  ovnval2  46670  hoicvr  46673  ovncvrrp  46689  ovn0lem  46690  ovnsubaddlem1  46695  hsphoif  46701  hsphoival  46704  hoidmv1le  46719  hoidmvlelem3  46722  ovnhoilem2  46727  ovncvr2  46736  hoidifhspval2  46740  hoidifhspval3  46744  hspmbllem2  46752  smfid  46877  fsetsnf1  47179  fsetsnfo  47180  cfsetsnfsetfv  47184  cfsetsnfsetfo  47187  fvmptrab  47419  fundcmpsurinjlem3  47527  sprval  47606  prproropreud  47636  upgrimwlklem3  48026  grtri  48067  stgrfv  48080  isubgr3stgrlem5  48097  rngcvalALTV  48392  rngcidALTV  48401  rhmsubcALTVlem3  48410  ringcvalALTV  48416  funcringcsetcALTV2lem1  48417  ringcidALTV  48435  funcringcsetclem1ALTV  48440  scmsuppss  48498  ply1mulgsum  48518  lindslinindsimp1  48585  lindsrng01  48596  islindeps2  48611  fdivmptfv  48673  refdivmptfv  48674  1arympt1fv  48767  itcoval0  48790  itcoval1  48791  itcoval2  48792  itcoval3  48793  itcovalsuc  48795  ackvalsuc1mpt  48806  ackvalsuc1  48807  ackval1  48809  ackval2  48810  ackval3  48811  ackval0val  48814  swapf1a  49397  swapf2a  49399  swapf1  49400  swapf2  49402  tposcurf2val  49429  fuco23  49469  prcof1  49516  prcof21a  49519  mndtcid  49717  amgmwlem  49930