Theorem fvmptd 7011

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

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1533   ∈ wcel 2098   ↦ cmpt 5232  ‘cfv 6549

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pr 5429

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5576  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-iota 6501  df-fun 6551  df-fv 6557

This theorem is referenced by:  fvmptd2  7012  fvmptdv2  7022  fvmptd4  7028  mptcnfimad  7991  fsplitfpar  8123  mpocurryvald  8276  fsetfocdm  8880  ttukeylem3  10536  ccatval1  14563  ccatval2  14564  repswsymb  14760  relexp1g  15009  rtrclreclem1  15040  rtrclreclem4  15044  dfrtrcl2  15045  prmodvdslcmf  17019  prmgap  17031  prmgaplcm  17032  prmgapprmo  17034  prdsvscafval  17465  mrcval  17593  cidval  17660  subcid  17836  idfu2nd  17866  resf2nd  17884  fuccoval  17958  fucid  17966  homaval  18023  idaval  18050  setcid  18078  catcid  18099  estrcid  18127  funcestrcsetclem1  18134  funcsetcestrclem1  18148  prf1  18194  prf2  18196  curf1  18220  curf11  18221  curf2val  18225  hof2  18252  yonedalem4a  18270  vrmdval  18817  smndex1gbas  18862  smndex1gid  18863  smndex1n0mnd  18872  mulgnngsum  19042  pj1val  19662  dpjval  20025  c0mgm  20410  c0mhm  20411  c0snmgmhm  20413  c0snmhm  20414  zrrnghm  20485  zrinitorngc  20587  zrtermorngc  20588  zrtermoringc  20620  sraval  21072  rngqiprngimfv  21205  frlmphl  21732  opsrval  22006  selvfval  22082  selvval  22083  mhpval  22087  mhpsclcl  22094  mhpmulcl  22096  psdfval  22105  psdval  22106  psdcoef  22107  cply1mul  22240  cply1coe0  22245  cply1coe0bi  22246  gsummoncoe1  22252  evls1sca  22267  mvmulfv  22490  mavmulfv  22492  mdetuni0  22567  mat2pmatval  22670  m2cpm  22687  cpm2mval  22696  m2cpminvid2lem  22700  decpmatid  22716  decpmatmullem  22717  pmatcollpw2lem  22723  monmatcollpw  22725  pm2mpfval  22742  mp2pm2mplem4  22755  pm2mpmhmlem2  22765  chpmatval  22777  fcfval  23981  cnextfval  24010  utopsnneiplem  24196  rrxmvallem  25376  rrxmval  25377  itgpowd  26029  taylpval  26346  lgamgulmlem2  27007  lgamcvglem  27017  logexprlim  27203  dchr1  27235  ishlg  28478  mirval  28531  mirfv  28532  ishpg  28635  lmif  28661  islmib  28663  lmodvslmhm  32854  psgnfzto1stlem  32913  tocycfv  32922  sgnsval  32974  evls1fldgencl  33486  minplyval  33504  madjusmdetlem2  33557  zarcls0  33597  zarcls1  33598  zarclsiin  33600  zarclsint  33601  zarclssn  33602  qqhvval  33712  indval  33760  indfval  33763  esummulc1  33828  esumcvg  33833  ofcval  33846  sigagenval  33887  measinb  33968  omsfval  34042  omssubadd  34048  sitgfval  34089  eulerpartlemsv1  34104  eulerpartlems  34108  fibp1  34149  totprobd  34174  probmeasb  34178  dstrvprob  34219  dstfrvinc  34224  dstfrvclim1  34225  ballotlemfval  34237  ballotlemsv  34257  gsumnunsn  34301  signsply0  34311  signstfval  34324  fdvneggt  34360  fdvnegge  34362  itgexpif  34366  breprexplema  34390  vtsval  34397  logdivsqrle  34410  hgt750lemg  34414  afsval  34431  lpadval  34436  cvmliftlem9  35031  goel  35085  satf0suc  35114  sat1el2xp  35117  fmlafv  35118  fmla  35119  fmlasuc0  35122  ex-sategoelel  35159  ex-sategoelelomsuc  35164  mvrsval  35243  mrsubfval  35246  mrsubval  35247  msubfval  35262  msubval  35263  msrval  35276  fwddifval  35886  fwddifnval  35887  knoppcnlem1  36096  knoppcnlem4  36099  knoppcnlem6  36101  knoppcnlem7  36102  bj-imdirval2  36790  bj-iminvval2  36801  bj-fvmptunsn2  36865  bj-endval  36922  poimirlem1  37222  poimirlem2  37223  poimirlem5  37226  poimirlem6  37227  poimirlem7  37228  poimirlem10  37231  poimirlem11  37232  poimirlem12  37233  poimirlem19  37240  poimirlem22  37243  mblfinlem2  37259  areacirc  37314  tendopl2  40377  tendoi2  40395  erngplus2  40404  erngplus2-rN  40412  hlhilset  41534  rhmzrhval  41569  lcmineqlem12  41640  aks4d1p9  41688  primrootscoprbij  41702  aks6d1c1p3  41710  aks6d1c1p5  41712  aks6d1c1  41716  hashscontpow  41722  aks6d1c3  41723  aks6d1c4  41724  aks6d1c2lem4  41727  aks6d1c2  41730  aks6d1c5lem3  41737  deg1gprod  41740  sticksstones2  41747  sticksstones3  41748  sticksstones6  41751  sticksstones7  41752  sticksstones8  41753  sticksstones10  41755  sticksstones12a  41757  sticksstones12  41758  sticksstones17  41763  sticksstones18  41764  sticksstones19  41765  aks6d1c6lem1  41770  aks6d1c6lem2  41771  aks6d1c6lem3  41772  aks6d1c6lem4  41773  aks6d1c6isolem1  41774  aks6d1c6isolem2  41775  aks6d1c6isolem3  41776  aks6d1c6lem5  41777  aks6d1c7lem1  41780  aks5lem2  41787  metakunt3  41790  metakunt4  41791  metakunt5  41792  metakunt6  41793  metakunt7  41794  metakunt8  41795  metakunt10  41797  metakunt11  41798  metakunt12  41799  metakunt20  41807  metakunt21  41808  metakunt22  41809  metakunt26  41813  metakunt27  41814  metakunt28  41815  metakunt29  41816  metakunt30  41817  metakunt32  41819  rfovfvd  43571  rfovfvfvd  43572  rfovcnvf1od  43573  rfovcnvfvd  43576  fsovfvd  43579  fsovfvfvd  43580  fsovcnvlem  43582  dssmapfv2d  43587  dssmapfv3d  43588  dssmapnvod  43589  clsk3nimkb  43609  dvgrat  43888  radcnvrat  43890  hashnzfzclim  43898  binomcxplemnn0  43925  binomcxplemrat  43926  binomcxplemfrat  43927  binomcxplemradcnv  43928  binomcxplemcvg  43930  binomcxplemdvsum  43931  binomcxplemnotnn0  43932  mapss2  44714  fmuldfeqlem1  45105  clim1fr1  45124  climrec  45126  climexp  45128  climneg  45133  divcnvg  45150  sumnnodd  45153  supcnvlimsup  45263  icccncfext  45410  cncfioobdlem  45419  fprodsubrecnncnvlem  45430  fprodaddrecnncnvlem  45432  dvsinax  45436  fperdvper  45442  dvcosax  45449  ioodvbdlimc1lem2  45455  ioodvbdlimc2lem  45457  dvnmul  45466  dvnprodlem1  45469  dvnprodlem2  45470  dvnprodlem3  45471  itgsinexp  45478  itgcoscmulx  45492  itgsincmulx  45497  itgsubsticclem  45498  itgsubsticc  45499  itgiccshift  45503  wallispilem5  45592  wallispi  45593  wallispi2lem1  45594  wallispi2lem2  45595  wallispi2  45596  stirlinglem1  45597  stirlinglem2  45598  stirlinglem3  45599  stirlinglem4  45600  stirlinglem5  45601  stirlinglem7  45603  stirlinglem8  45604  stirlinglem10  45606  stirlinglem11  45607  stirlinglem12  45608  stirlinglem13  45609  stirlinglem14  45610  stirlinglem15  45611  dirkerval2  45617  dirkercncflem2  45627  fourierdlem7  45637  fourierdlem13  45643  fourierdlem14  45644  fourierdlem16  45646  fourierdlem18  45648  fourierdlem19  45649  fourierdlem21  45651  fourierdlem22  45652  fourierdlem26  45656  fourierdlem37  45667  fourierdlem39  45669  fourierdlem41  45671  fourierdlem48  45677  fourierdlem49  45678  fourierdlem50  45679  fourierdlem51  45680  fourierdlem53  45682  fourierdlem62  45691  fourierdlem63  45692  fourierdlem65  45694  fourierdlem73  45702  fourierdlem74  45703  fourierdlem75  45704  fourierdlem76  45705  fourierdlem79  45708  fourierdlem81  45710  fourierdlem82  45711  fourierdlem83  45712  fourierdlem84  45713  fourierdlem88  45717  fourierdlem89  45718  fourierdlem90  45719  fourierdlem91  45720  fourierdlem92  45721  fourierdlem93  45722  fourierdlem97  45726  fourierdlem101  45730  fourierdlem103  45732  fourierdlem104  45733  fourierdlem111  45740  fourierdlem112  45741  fouriersw  45754  elaa2lem  45756  etransclem13  45770  etransclem17  45774  etransclem18  45775  etransclem21  45778  etransclem31  45788  etransclem32  45789  etransclem33  45790  etransclem35  45792  etransclem46  45803  etransclem48  45805  rrxtopnfi  45810  salgenval  45844  sge0val  45889  sge0z  45898  sge0snmpt  45906  sge0xp  45952  nnfoctbdjlem  45978  omeiunltfirp  46042  caratheodorylem1  46049  0ome  46052  ovnval2  46068  hoicvr  46071  ovncvrrp  46087  ovn0lem  46088  ovnsubaddlem1  46093  hsphoif  46099  hsphoival  46102  hoidmv1le  46117  hoidmvlelem3  46120  ovnhoilem2  46125  ovncvr2  46134  hoidifhspval2  46138  hoidifhspval3  46142  hspmbllem2  46150  smfid  46275  fsetsnf1  46569  fsetsnfo  46570  cfsetsnfsetfv  46574  cfsetsnfsetfo  46577  fvmptrab  46807  fundcmpsurinjlem3  46874  sprval  46953  prproropreud  46983  rngcvalALTV  47510  rngcidALTV  47519  rhmsubcALTVlem3  47528  ringcvalALTV  47534  funcringcsetcALTV2lem1  47535  ringcidALTV  47553  funcringcsetclem1ALTV  47558  scmsuppss  47619  ply1mulgsum  47641  lindslinindsimp1  47708  lindsrng01  47719  islindeps2  47734  fdivmptfv  47801  refdivmptfv  47802  1arympt1fv  47895  itcoval0  47918  itcoval1  47919  itcoval2  47920  itcoval3  47921  itcovalsuc  47923  ackvalsuc1mpt  47934  ackvalsuc1  47935  ackval1  47937  ackval2  47938  ackval3  47939  ackval0val  47942  mndtcid  48284  amgmwlem  48418