Theorem fvmptd 6999

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143   ↦ cmpt 5193  ‘cfv 6538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-iota 6494  df-fun 6540  df-fv 6546

This theorem is referenced by:  fvmptd2  7000  fvmptdv2  7010  fvmptd4  7016  mptcnfimad  7984  fsplitfpar  8114  mpocurryvald  8267  ttukeylem3  10496  indval  12222  indfval  12226  tpf1ofv0  14535  tpf1ofv1  14536  tpf1ofv2  14537  ccatval1  14616  ccatval2  14617  repswsymb  14813  relexp1g  15065  rtrclreclem1  15096  rtrclreclem4  15100  dfrtrcl2  15101  prmodvdslcmf  17108  prmgap  17120  prmgaplcm  17121  prmgapprmo  17123  prdsvscafval  17534  mrcval  17667  cidval  17734  subcid  17905  idfu2nd  17935  resf2nd  17953  fuccoval  18024  fucid  18032  homaval  18089  idaval  18116  setcid  18144  catcid  18165  estrcid  18191  funcestrcsetclem1  18197  funcsetcestrclem1  18211  prf1  18257  prf2  18259  curf1  18282  curf11  18283  curf2val  18287  hof2  18314  yonedalem4a  18332  vrmdval  18917  smndex1gbasOLD  18963  smndex1gid  18964  smndex1gidOLD  18965  smndex1n0mnd  18975  mulgnngsum  19146  pj1val  19766  dpjval  20129  c0mgm  20542  c0mhm  20543  c0snmgmhm  20545  c0snmhm  20546  zrrnghm  20622  zrinitorngc  20728  zrtermorngc  20729  zrtermoringc  20761  sraval  21277  rngqiprngimfv  21419  frlmphl  21912  opsrval  22178  selvfval  22251  mhpval  22283  mhpsclcl  22291  psdfval  22302  cply1mul  22437  cply1coe0  22442  cply1coe0bi  22443  gsummoncoe1  22449  evls1sca  22464  mvmulfv  22682  mavmulfv  22684  mdetuni0  22759  mat2pmatval  22862  m2cpm  22879  cpm2mval  22888  m2cpminvid2lem  22892  decpmatid  22908  decpmatmullem  22909  pmatcollpw2lem  22915  monmatcollpw  22917  pm2mpfval  22934  mp2pm2mplem4  22947  pm2mpmhmlem2  22957  chpmatval  22969  fcfval  24171  cnextfval  24200  utopsnneiplem  24385  rrxmvallem  25544  rrxmval  25545  itgpowd  26190  taylpval  26511  lgamgulmlem2  27175  lgamcvglem  27185  logexprlim  27370  dchr1  27402  ishlg  28855  mirval  28913  mirfv  28914  ishpg  29022  lmif  29075  islmib  29077  lmodvslmhm  33351  psgnfzto1stlem  33401  tocycfv  33410  sgnsval  33462  psrnzr  33883  0mplrim  33885  selvply1rhmlemb  33890  selvply1rhmlem2  33892  mplvrpmrhm  33918  esplyfval0  33935  esplyind  33946  evls1fldgencl  34041  minplyval  34076  rtelextdg2lem  34097  2sqr3minply  34151  cos9thpiminply  34159  zarcls0  34239  zarcls1  34240  zarclsiin  34242  zarclsint  34243  zarclssn  34244  qqhvval  34354  esummulc1  34452  esumcvg  34457  ofcval  34470  sigagenval  34511  measinb  34592  omsfval  34665  omssubadd  34671  sitgfval  34712  eulerpartlemsv1  34727  eulerpartlems  34731  fibp1  34772  totprobd  34797  probmeasb  34801  dstrvprob  34843  dstfrvinc  34848  dstfrvclim1  34849  ballotlemfval  34861  ballotlemsv  34881  gsumnunsn  34912  signsply0  34919  signstfval  34932  fdvneggt  34968  fdvnegge  34970  itgexpif  34974  breprexplema  34998  vtsval  35005  logdivsqrle  35018  hgt750lemg  35022  afsval  35042  lpadval  35047  cvmliftlem9  35766  goel  35820  satf0suc  35849  sat1el2xp  35852  fmlafv  35853  fmla  35854  fmlasuc0  35857  ex-sategoelel  35894  ex-sategoelelomsuc  35899  mvrsval  35978  mrsubfval  35981  mrsubval  35982  msubfval  35997  msubval  35998  msrval  36011  fwddifval  36635  fwddifnval  36636  knoppcnlem1  37063  knoppcnlem4  37066  knoppcnlem6  37068  knoppcnlem7  37069  bj-imdirval2  37808  bj-iminvval2  37819  bj-fvmptunsn2  37883  bj-endval  37940  poimirlem1  38253  poimirlem2  38254  poimirlem5  38257  poimirlem6  38258  poimirlem7  38259  poimirlem10  38262  poimirlem11  38263  poimirlem12  38264  poimirlem19  38271  poimirlem22  38274  mblfinlem2  38290  areacirc  38345  tendopl2  41532  tendoi2  41550  erngplus2  41559  erngplus2-rN  41567  hlhilset  42689  rhmzrhval  42720  lcmineqlem12  42788  aks4d1p9  42836  primrootscoprbij  42850  aks6d1c1p3  42858  aks6d1c1p5  42860  aks6d1c1  42864  hashscontpow  42870  aks6d1c3  42871  aks6d1c4  42872  aks6d1c2lem4  42875  aks6d1c2  42878  aks6d1c5lem3  42885  deg1gprod  42888  sticksstones2  42895  sticksstones3  42896  sticksstones6  42899  sticksstones7  42900  sticksstones8  42901  sticksstones10  42903  sticksstones12a  42905  sticksstones12  42906  sticksstones17  42911  sticksstones18  42912  sticksstones19  42913  aks6d1c6lem1  42918  aks6d1c6lem2  42919  aks6d1c6lem3  42920  aks6d1c6lem4  42921  aks6d1c6isolem1  42922  aks6d1c6isolem2  42923  aks6d1c6isolem3  42924  aks6d1c6lem5  42925  aks6d1c7lem1  42928  aks5lem2  42935  aks5lem3a  42937  unitscyglem1  42943  rfovfvd  44711  rfovfvfvd  44712  rfovcnvf1od  44713  rfovcnvfvd  44716  fsovfvd  44719  fsovfvfvd  44720  fsovcnvlem  44722  dssmapfv2d  44727  dssmapfv3d  44728  dssmapnvod  44729  clsk3nimkb  44749  dvgrat  45005  radcnvrat  45007  hashnzfzclim  45015  binomcxplemnn0  45042  binomcxplemrat  45043  binomcxplemfrat  45044  binomcxplemradcnv  45045  binomcxplemcvg  45047  binomcxplemdvsum  45048  binomcxplemnotnn0  45049  mapss2  45905  fmuldfeqlem1  46281  clim1fr1  46300  climrec  46302  climexp  46304  climneg  46309  divcnvg  46326  sumnnodd  46329  supcnvlimsup  46437  icccncfext  46584  cncfioobdlem  46593  fprodsubrecnncnvlem  46604  fprodaddrecnncnvlem  46606  dvsinax  46610  fperdvper  46616  dvcosax  46623  ioodvbdlimc1lem2  46629  ioodvbdlimc2lem  46631  dvnmul  46640  dvnprodlem1  46643  dvnprodlem2  46644  dvnprodlem3  46645  itgsinexp  46652  itgcoscmulx  46666  itgsincmulx  46671  itgsubsticclem  46672  itgsubsticc  46673  itgiccshift  46677  wallispilem5  46766  wallispi  46767  wallispi2lem1  46768  wallispi2lem2  46769  wallispi2  46770  stirlinglem1  46771  stirlinglem2  46772  stirlinglem3  46773  stirlinglem4  46774  stirlinglem5  46775  stirlinglem7  46777  stirlinglem8  46778  stirlinglem10  46780  stirlinglem11  46781  stirlinglem12  46782  stirlinglem13  46783  stirlinglem14  46784  stirlinglem15  46785  dirkerval2  46791  dirkercncflem2  46801  fourierdlem7  46811  fourierdlem13  46817  fourierdlem14  46818  fourierdlem16  46820  fourierdlem18  46822  fourierdlem19  46823  fourierdlem21  46825  fourierdlem22  46826  fourierdlem26  46830  fourierdlem37  46841  fourierdlem39  46843  fourierdlem41  46845  fourierdlem50  46853  fourierdlem51  46854  fourierdlem53  46856  fourierdlem62  46865  fourierdlem63  46866  fourierdlem65  46868  fourierdlem73  46876  fourierdlem74  46877  fourierdlem75  46878  fourierdlem76  46879  fourierdlem79  46882  fourierdlem81  46884  fourierdlem82  46885  fourierdlem83  46886  fourierdlem84  46887  fourierdlem88  46891  fourierdlem89  46892  fourierdlem90  46893  fourierdlem91  46894  fourierdlem92  46895  fourierdlem93  46896  fourierdlem97  46900  fourierdlem101  46904  fourierdlem103  46906  fourierdlem104  46907  fourierdlem111  46914  fourierdlem112  46915  fouriersw  46928  elaa2lem  46930  etransclem13  46944  etransclem17  46948  etransclem18  46949  etransclem21  46952  etransclem31  46962  etransclem32  46963  etransclem33  46964  etransclem35  46966  etransclem46  46977  etransclem48  46979  rrxtopnfi  46984  salgenval  47018  sge0val  47063  sge0z  47072  sge0snmpt  47080  sge0xp  47126  nnfoctbdjlem  47152  omeiunltfirp  47216  caratheodorylem1  47223  0ome  47226  ovnval2  47242  hoicvr  47245  ovncvrrp  47261  ovn0lem  47262  ovnsubaddlem1  47267  hsphoif  47273  hsphoival  47276  hoidmv1le  47291  hoidmvlelem3  47294  ovnhoilem2  47299  ovncvr2  47308  hoidifhspval2  47312  hoidifhspval3  47316  hspmbllem2  47324  smfid  47449  fsetsnf1  47772  fsetsnfo  47773  cfsetsnfsetfv  47777  cfsetsnfsetfo  47780  fvmptrab  48012  fundcmpsurinjlem3  48132  sprval  48211  prproropreud  48241  upgrimwlklem3  48647  grtri  48688  stgrfv  48701  isubgr3stgrlem5  48718  rngcvalALTV  49013  rngcidALTV  49022  rhmsubcALTVlem3  49031  ringcvalALTV  49037  funcringcsetcALTV2lem1  49038  ringcidALTV  49056  funcringcsetclem1ALTV  49061  scmsuppss  49134  ply1mulgsum  49153  lindslinindsimp1  49220  lindsrng01  49231  islindeps2  49246  fdivmptfv  49308  refdivmptfv  49309  1arympt1fv  49402  itcoval0  49425  itcoval1  49426  itcoval2  49427  itcoval3  49428  itcovalsuc  49430  ackvalsuc1mpt  49441  ackvalsuc1  49442  ackval1  49444  ackval2  49445  ackval3  49446  ackval0val  49449  swapf1a  50030  swapf2a  50032  swapf1  50033  swapf2  50035  tposcurf2val  50062  fuco23  50102  prcof1  50149  prcof21a  50152  mndtcid  50350  amgmwlem  50585