Theorem fvmptd 6752

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111   ↦ cmpt 5110  ‘cfv 6324

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-iota 6283  df-fun 6326  df-fv 6332

This theorem is referenced by:  fvmptd2  6753  fvmptdv2  6763  fsplitfpar  7797  mpocurryvald  7919  ttukeylem3  9922  ccatval1  13921  ccatval1OLD  13922  ccatval2  13923  repswsymb  14127  relexp1g  14377  rtrclreclem1  14408  rtrclreclem4  14412  dfrtrcl2  14413  prmodvdslcmf  16373  prmgap  16385  prmgaplcm  16386  prmgapprmo  16388  prdsvscafval  16745  mrcval  16873  cidval  16940  subcid  17109  idfu2nd  17139  resf2nd  17157  fuccoval  17225  fucid  17233  homaval  17283  idaval  17310  setcid  17338  catcid  17355  estrcid  17376  funcestrcsetclem1  17382  funcsetcestrclem1  17396  prf1  17442  prf2  17444  curf1  17467  curf11  17468  curf2val  17472  hof2  17499  yonedalem4a  17517  vrmdval  18014  smndex1gbas  18059  smndex1gid  18060  smndex1n0mnd  18069  mulgnngsum  18225  pj1val  18813  dpjval  19171  sraval  19941  frlmphl  20470  opsrval  20714  selvfval  20789  selvval  20790  mhpval  20792  cply1mul  20923  cply1coe0  20928  cply1coe0bi  20929  gsummoncoe1  20933  evls1sca  20947  mvmulfv  21149  mavmulfv  21151  mdetuni0  21226  mat2pmatval  21329  m2cpm  21346  cpm2mval  21355  m2cpminvid2lem  21359  decpmatid  21375  decpmatmullem  21376  pmatcollpw2lem  21382  monmatcollpw  21384  pm2mpfval  21401  mp2pm2mplem4  21414  pm2mpmhmlem2  21424  chpmatval  21436  fcfval  22638  cnextfval  22667  utopsnneiplem  22853  rrxmvallem  24008  rrxmval  24009  itgpowd  24653  taylpval  24962  lgamgulmlem2  25615  lgamcvglem  25625  logexprlim  25809  dchr1  25841  ishlg  26396  mirval  26449  mirfv  26450  ishpg  26553  lmif  26579  islmib  26581  lmodvslmhm  30735  psgnfzto1stlem  30792  tocycfv  30801  sgnsval  30853  madjusmdetlem2  31181  zarcls0  31221  zarcls1  31222  zarclsiin  31224  zarclsint  31225  zarclssn  31226  metidval  31243  pstmval  31248  qqhvval  31334  indval  31382  indfval  31385  esummulc1  31450  esumcvg  31455  ofcval  31468  sigagenval  31509  measinb  31590  omsfval  31662  omssubadd  31668  sitgfval  31709  eulerpartlemsv1  31724  eulerpartlems  31728  fibp1  31769  totprobd  31794  probmeasb  31798  dstrvprob  31839  dstfrvinc  31844  dstfrvclim1  31845  ballotlemfval  31857  ballotlemsv  31877  gsumnunsn  31921  signsply0  31931  signstfval  31944  fdvneggt  31981  fdvnegge  31983  itgexpif  31987  breprexplema  32011  vtsval  32018  logdivsqrle  32031  hgt750lemg  32035  afsval  32052  lpadval  32057  cvmliftlem9  32653  goel  32707  satf0suc  32736  sat1el2xp  32739  fmlafv  32740  fmla  32741  fmlasuc0  32744  ex-sategoelel  32781  ex-sategoelelomsuc  32786  mvrsval  32865  mrsubfval  32868  mrsubval  32869  msubfval  32884  msubval  32885  msrval  32898  fwddifval  33736  fwddifnval  33737  knoppcnlem1  33945  knoppcnlem4  33948  knoppcnlem6  33950  knoppcnlem7  33951  bj-imdirval2  34598  bj-iminvval2  34609  bj-fvmptunsn2  34673  bj-endval  34729  poimirlem1  35058  poimirlem2  35059  poimirlem5  35062  poimirlem6  35063  poimirlem7  35064  poimirlem10  35067  poimirlem11  35068  poimirlem12  35069  poimirlem19  35076  poimirlem22  35079  mblfinlem2  35095  areacirc  35150  tendopl2  38073  tendoi2  38091  erngplus2  38100  erngplus2-rN  38108  hlhilset  39230  lcmineqlem12  39328  metakunt3  39352  metakunt4  39353  metakunt5  39354  metakunt6  39355  metakunt7  39356  metakunt8  39357  metakunt10  39359  metakunt11  39360  metakunt12  39361  metakunt20  39369  metakunt21  39370  metakunt22  39371  metakunt26  39375  metakunt27  39376  metakunt28  39377  metakunt29  39378  metakunt30  39379  metakunt32  39381  rfovfvd  40703  rfovfvfvd  40704  rfovcnvf1od  40705  rfovcnvfvd  40708  fsovfvd  40711  fsovfvfvd  40712  fsovcnvlem  40714  dssmapfv2d  40719  dssmapfv3d  40720  dssmapnvod  40721  clsk3nimkb  40743  dvgrat  41016  radcnvrat  41018  hashnzfzclim  41026  binomcxplemnn0  41053  binomcxplemrat  41054  binomcxplemfrat  41055  binomcxplemradcnv  41056  binomcxplemcvg  41058  binomcxplemdvsum  41059  binomcxplemnotnn0  41060  mapss2  41834  fmuldfeqlem1  42224  clim1fr1  42243  climrec  42245  climexp  42247  climneg  42252  divcnvg  42269  sumnnodd  42272  supcnvlimsup  42382  icccncfext  42529  cncfioobdlem  42538  fprodsubrecnncnvlem  42549  fprodaddrecnncnvlem  42551  dvsinax  42555  fperdvper  42561  dvcosax  42568  ioodvbdlimc1lem2  42574  ioodvbdlimc2lem  42576  dvnmul  42585  dvnprodlem1  42588  dvnprodlem2  42589  dvnprodlem3  42590  itgsinexp  42597  itgcoscmulx  42611  itgsincmulx  42616  itgsubsticclem  42617  itgsubsticc  42618  itgiccshift  42622  wallispilem5  42711  wallispi  42712  wallispi2lem1  42713  wallispi2lem2  42714  wallispi2  42715  stirlinglem1  42716  stirlinglem2  42717  stirlinglem3  42718  stirlinglem4  42719  stirlinglem5  42720  stirlinglem7  42722  stirlinglem8  42723  stirlinglem10  42725  stirlinglem11  42726  stirlinglem12  42727  stirlinglem13  42728  stirlinglem14  42729  stirlinglem15  42730  dirkerval2  42736  dirkercncflem2  42746  fourierdlem7  42756  fourierdlem13  42762  fourierdlem14  42763  fourierdlem16  42765  fourierdlem18  42767  fourierdlem19  42768  fourierdlem21  42770  fourierdlem22  42771  fourierdlem26  42775  fourierdlem37  42786  fourierdlem39  42788  fourierdlem41  42790  fourierdlem48  42796  fourierdlem49  42797  fourierdlem50  42798  fourierdlem51  42799  fourierdlem53  42801  fourierdlem62  42810  fourierdlem63  42811  fourierdlem65  42813  fourierdlem73  42821  fourierdlem74  42822  fourierdlem75  42823  fourierdlem76  42824  fourierdlem79  42827  fourierdlem81  42829  fourierdlem82  42830  fourierdlem83  42831  fourierdlem84  42832  fourierdlem88  42836  fourierdlem89  42837  fourierdlem90  42838  fourierdlem91  42839  fourierdlem92  42840  fourierdlem93  42841  fourierdlem97  42845  fourierdlem101  42849  fourierdlem103  42851  fourierdlem104  42852  fourierdlem111  42859  fourierdlem112  42860  fouriersw  42873  elaa2lem  42875  etransclem13  42889  etransclem17  42893  etransclem18  42894  etransclem21  42897  etransclem31  42907  etransclem32  42908  etransclem33  42909  etransclem35  42911  etransclem46  42922  etransclem48  42924  rrxtopnfi  42929  salgenval  42963  sge0val  43005  sge0z  43014  sge0snmpt  43022  sge0xp  43068  nnfoctbdjlem  43094  omeiunltfirp  43158  caratheodorylem1  43165  0ome  43168  ovnval2  43184  hoicvr  43187  ovncvrrp  43203  ovn0lem  43204  ovnsubaddlem1  43209  hsphoif  43215  hsphoival  43218  hoidmv1le  43233  hoidmvlelem3  43236  ovnhoilem2  43241  ovncvr2  43250  hoidifhspval2  43254  hoidifhspval3  43258  hspmbllem2  43266  smfid  43386  fvmptrab  43848  fundcmpsurinjlem3  43917  sprval  43996  prproropreud  44026  isomuspgrlem2a  44346  c0mgm  44533  c0mhm  44534  c0snmgmhm  44538  c0snmhm  44539  zrrnghm  44541  rngcvalALTV  44585  rngcidALTV  44615  zrinitorngc  44624  zrtermorngc  44625  ringcvalALTV  44631  funcringcsetcALTV2lem1  44660  ringcidALTV  44678  funcringcsetclem1ALTV  44683  zrtermoringc  44694  rhmsubcALTVlem3  44730  scmsuppss  44774  ply1mulgsum  44798  lindslinindsimp1  44866  lindsrng01  44877  islindeps2  44892  fdivmptfv  44959  refdivmptfv  44960  1arympt1fv  45053  itcoval0  45076  itcoval1  45077  itcoval2  45078  itcoval3  45079  itcovalsuc  45081  ackvalsuc1mpt  45092  ackvalsuc1  45093  ackval1  45095  ackval2  45096  ackval3  45097  ackval0val  45100  amgmwlem  45330