Theorem fvmptd 6977

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1559   ∈ wcel 2141   ↦ cmpt 5178  ‘cfv 6515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-pr 5387

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5538  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-iota 6471  df-fun 6517  df-fv 6523

This theorem is referenced by:  fvmptd2  6978  fvmptdv2  6988  fvmptd4  6994  mptcnfimad  7961  fsplitfpar  8090  mpocurryvald  8243  ttukeylem3  10461  indval  12191  indfval  12195  tpf1ofv0  14502  tpf1ofv1  14503  tpf1ofv2  14504  ccatval1  14583  ccatval2  14584  repswsymb  14780  relexp1g  15032  rtrclreclem1  15063  rtrclreclem4  15067  dfrtrcl2  15068  prmodvdslcmf  17073  prmgap  17085  prmgaplcm  17086  prmgapprmo  17088  prdsvscafval  17499  mrcval  17632  cidval  17699  subcid  17870  idfu2nd  17900  resf2nd  17918  fuccoval  17989  fucid  17997  homaval  18054  idaval  18081  setcid  18109  catcid  18130  estrcid  18156  funcestrcsetclem1  18162  funcsetcestrclem1  18176  prf1  18222  prf2  18224  curf1  18247  curf11  18248  curf2val  18252  hof2  18279  yonedalem4a  18297  vrmdval  18881  smndex1gbasOLD  18927  smndex1gid  18928  smndex1gidOLD  18929  smndex1n0mnd  18939  mulgnngsum  19111  pj1val  19725  dpjval  20088  c0mgm  20494  c0mhm  20495  c0snmgmhm  20497  c0snmhm  20498  zrrnghm  20572  zrinitorngc  20678  zrtermorngc  20679  zrtermoringc  20711  sraval  21229  rngqiprngimfv  21355  frlmphl  21820  opsrval  22086  selvfval  22159  mhpval  22191  mhpsclcl  22199  psdfval  22210  cply1mul  22346  cply1coe0  22351  cply1coe0bi  22352  gsummoncoe1  22358  evls1sca  22373  mvmulfv  22591  mavmulfv  22593  mdetuni0  22668  mat2pmatval  22771  m2cpm  22788  cpm2mval  22797  m2cpminvid2lem  22801  decpmatid  22817  decpmatmullem  22818  pmatcollpw2lem  22824  monmatcollpw  22826  pm2mpfval  22843  mp2pm2mplem4  22856  pm2mpmhmlem2  22866  chpmatval  22878  fcfval  24080  cnextfval  24109  utopsnneiplem  24294  rrxmvallem  25453  rrxmval  25454  itgpowd  26099  taylpval  26417  lgamgulmlem2  27081  lgamcvglem  27091  logexprlim  27276  dchr1  27308  ishlg  28758  mirval  28811  mirfv  28812  ishpg  28915  lmif  28941  islmib  28943  lmodvslmhm  33190  psgnfzto1stlem  33240  tocycfv  33249  sgnsval  33301  psrnzr  33769  0mplrim  33771  selvply1rhmlemb  33776  selvply1rhmlem2  33778  mplvrpmrhm  33804  esplyfval0  33821  esplyind  33832  evls1fldgencl  33927  minplyval  33962  rtelextdg2lem  33983  2sqr3minply  34037  cos9thpiminply  34045  zarcls0  34125  zarcls1  34126  zarclsiin  34128  zarclsint  34129  zarclssn  34130  qqhvval  34240  esummulc1  34338  esumcvg  34343  ofcval  34356  sigagenval  34397  measinb  34478  omsfval  34551  omssubadd  34557  sitgfval  34598  eulerpartlemsv1  34613  eulerpartlems  34617  fibp1  34658  totprobd  34683  probmeasb  34687  dstrvprob  34729  dstfrvinc  34734  dstfrvclim1  34735  ballotlemfval  34747  ballotlemsv  34767  gsumnunsn  34798  signsply0  34805  signstfval  34818  fdvneggt  34854  fdvnegge  34856  itgexpif  34860  breprexplema  34884  vtsval  34891  logdivsqrle  34904  hgt750lemg  34908  afsval  34928  lpadval  34933  cvmliftlem9  35603  goel  35657  satf0suc  35686  sat1el2xp  35689  fmlafv  35690  fmla  35691  fmlasuc0  35694  ex-sategoelel  35731  ex-sategoelelomsuc  35736  mvrsval  35815  mrsubfval  35818  mrsubval  35819  msubfval  35834  msubval  35835  msrval  35848  fwddifval  36472  fwddifnval  36473  knoppcnlem1  36891  knoppcnlem4  36894  knoppcnlem6  36896  knoppcnlem7  36897  bj-imdirval2  37635  bj-iminvval2  37646  bj-fvmptunsn2  37710  bj-endval  37767  poimirlem1  38080  poimirlem2  38081  poimirlem5  38084  poimirlem6  38085  poimirlem7  38086  poimirlem10  38089  poimirlem11  38090  poimirlem12  38091  poimirlem19  38098  poimirlem22  38101  mblfinlem2  38117  areacirc  38172  tendopl2  41361  tendoi2  41379  erngplus2  41388  erngplus2-rN  41396  hlhilset  42518  rhmzrhval  42549  lcmineqlem12  42617  aks4d1p9  42665  primrootscoprbij  42679  aks6d1c1p3  42687  aks6d1c1p5  42689  aks6d1c1  42693  hashscontpow  42699  aks6d1c3  42700  aks6d1c4  42701  aks6d1c2lem4  42704  aks6d1c2  42707  aks6d1c5lem3  42714  deg1gprod  42717  sticksstones2  42724  sticksstones3  42725  sticksstones6  42728  sticksstones7  42729  sticksstones8  42730  sticksstones10  42732  sticksstones12a  42734  sticksstones12  42735  sticksstones17  42740  sticksstones18  42741  sticksstones19  42742  aks6d1c6lem1  42747  aks6d1c6lem2  42748  aks6d1c6lem3  42749  aks6d1c6lem4  42750  aks6d1c6isolem1  42751  aks6d1c6isolem2  42752  aks6d1c6isolem3  42753  aks6d1c6lem5  42754  aks6d1c7lem1  42757  aks5lem2  42764  aks5lem3a  42766  unitscyglem1  42772  rfovfvd  44538  rfovfvfvd  44539  rfovcnvf1od  44540  rfovcnvfvd  44543  fsovfvd  44546  fsovfvfvd  44547  fsovcnvlem  44549  dssmapfv2d  44554  dssmapfv3d  44555  dssmapnvod  44556  clsk3nimkb  44576  dvgrat  44848  radcnvrat  44850  hashnzfzclim  44858  binomcxplemnn0  44885  binomcxplemrat  44886  binomcxplemfrat  44887  binomcxplemradcnv  44888  binomcxplemcvg  44890  binomcxplemdvsum  44891  binomcxplemnotnn0  44892  mapss2  45742  fmuldfeqlem1  46118  clim1fr1  46137  climrec  46139  climexp  46141  climneg  46146  divcnvg  46163  sumnnodd  46166  supcnvlimsup  46274  icccncfext  46421  cncfioobdlem  46430  fprodsubrecnncnvlem  46441  fprodaddrecnncnvlem  46443  dvsinax  46447  fperdvper  46453  dvcosax  46460  ioodvbdlimc1lem2  46466  ioodvbdlimc2lem  46468  dvnmul  46477  dvnprodlem1  46480  dvnprodlem2  46481  dvnprodlem3  46482  itgsinexp  46489  itgcoscmulx  46503  itgsincmulx  46508  itgsubsticclem  46509  itgsubsticc  46510  itgiccshift  46514  wallispilem5  46603  wallispi  46604  wallispi2lem1  46605  wallispi2lem2  46606  wallispi2  46607  stirlinglem1  46608  stirlinglem2  46609  stirlinglem3  46610  stirlinglem4  46611  stirlinglem5  46612  stirlinglem7  46614  stirlinglem8  46615  stirlinglem10  46617  stirlinglem11  46618  stirlinglem12  46619  stirlinglem13  46620  stirlinglem14  46621  stirlinglem15  46622  dirkerval2  46628  dirkercncflem2  46638  fourierdlem7  46648  fourierdlem13  46654  fourierdlem14  46655  fourierdlem16  46657  fourierdlem18  46659  fourierdlem19  46660  fourierdlem21  46662  fourierdlem22  46663  fourierdlem26  46667  fourierdlem37  46678  fourierdlem39  46680  fourierdlem41  46682  fourierdlem50  46690  fourierdlem51  46691  fourierdlem53  46693  fourierdlem62  46702  fourierdlem63  46703  fourierdlem65  46705  fourierdlem73  46713  fourierdlem74  46714  fourierdlem75  46715  fourierdlem76  46716  fourierdlem79  46719  fourierdlem81  46721  fourierdlem82  46722  fourierdlem83  46723  fourierdlem84  46724  fourierdlem88  46728  fourierdlem89  46729  fourierdlem90  46730  fourierdlem91  46731  fourierdlem92  46732  fourierdlem93  46733  fourierdlem97  46737  fourierdlem101  46741  fourierdlem103  46743  fourierdlem104  46744  fourierdlem111  46751  fourierdlem112  46752  fouriersw  46765  elaa2lem  46767  etransclem13  46781  etransclem17  46785  etransclem18  46786  etransclem21  46789  etransclem31  46799  etransclem32  46800  etransclem33  46801  etransclem35  46803  etransclem46  46814  etransclem48  46816  rrxtopnfi  46821  salgenval  46855  sge0val  46900  sge0z  46909  sge0snmpt  46917  sge0xp  46963  nnfoctbdjlem  46989  omeiunltfirp  47053  caratheodorylem1  47060  0ome  47063  ovnval2  47079  hoicvr  47082  ovncvrrp  47098  ovn0lem  47099  ovnsubaddlem1  47104  hsphoif  47110  hsphoival  47113  hoidmv1le  47128  hoidmvlelem3  47131  ovnhoilem2  47136  ovncvr2  47145  hoidifhspval2  47149  hoidifhspval3  47153  hspmbllem2  47161  smfid  47286  fsetsnf1  47606  fsetsnfo  47607  cfsetsnfsetfv  47611  cfsetsnfsetfo  47614  fvmptrab  47846  fundcmpsurinjlem3  47966  sprval  48045  prproropreud  48075  upgrimwlklem3  48481  grtri  48522  stgrfv  48535  isubgr3stgrlem5  48552  rngcvalALTV  48847  rngcidALTV  48856  rhmsubcALTVlem3  48865  ringcvalALTV  48871  funcringcsetcALTV2lem1  48872  ringcidALTV  48890  funcringcsetclem1ALTV  48895  scmsuppss  48953  ply1mulgsum  48972  lindslinindsimp1  49039  lindsrng01  49050  islindeps2  49065  fdivmptfv  49127  refdivmptfv  49128  1arympt1fv  49221  itcoval0  49244  itcoval1  49245  itcoval2  49246  itcoval3  49247  itcovalsuc  49249  ackvalsuc1mpt  49260  ackvalsuc1  49261  ackval1  49263  ackval2  49264  ackval3  49265  ackval0val  49268  swapf1a  49850  swapf2a  49852  swapf1  49853  swapf2  49855  tposcurf2val  49882  fuco23  49922  prcof1  49969  prcof21a  49972  mndtcid  50170  amgmwlem  50383