Theorem fvmptd 6987

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1563   ∈ wcel 2145   ↦ cmpt 5185  ‘cfv 6525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5250  ax-pr 5394

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-sbc 3748  df-csb 3856  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5105  df-opab 5167  df-mpt 5186  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-iota 6481  df-fun 6527  df-fv 6533

This theorem is referenced by:  fvmptd2  6988  fvmptdv2  6998  fvmptd4  7004  mptcnfimad  7971  fsplitfpar  8101  mpocurryvald  8254  ttukeylem3  10483  indval  12209  indfval  12213  tpf1ofv0  14521  tpf1ofv1  14522  tpf1ofv2  14523  ccatval1  14602  ccatval2  14603  repswsymb  14799  relexp1g  15051  rtrclreclem1  15082  rtrclreclem4  15086  dfrtrcl2  15087  prmodvdslcmf  17095  prmgap  17107  prmgaplcm  17108  prmgapprmo  17110  prdsvscafval  17521  mrcval  17654  cidval  17721  subcid  17892  idfu2nd  17922  resf2nd  17940  fuccoval  18011  fucid  18019  homaval  18076  idaval  18103  setcid  18131  catcid  18152  estrcid  18178  funcestrcsetclem1  18184  funcsetcestrclem1  18198  prf1  18244  prf2  18246  curf1  18269  curf11  18270  curf2val  18274  hof2  18301  yonedalem4a  18319  vrmdval  18904  smndex1gbasOLD  18950  smndex1gid  18951  smndex1gidOLD  18952  smndex1n0mnd  18962  mulgnngsum  19133  pj1val  19753  dpjval  20116  c0mgm  20529  c0mhm  20530  c0snmgmhm  20532  c0snmhm  20533  zrrnghm  20609  zrinitorngc  20715  zrtermorngc  20716  zrtermoringc  20748  sraval  21262  rngqiprngimfv  21397  frlmphl  21888  opsrval  22154  selvfval  22227  mhpval  22259  mhpsclcl  22267  psdfval  22278  cply1mul  22413  cply1coe0  22418  cply1coe0bi  22419  gsummoncoe1  22425  evls1sca  22440  mvmulfv  22658  mavmulfv  22660  mdetuni0  22735  mat2pmatval  22838  m2cpm  22855  cpm2mval  22864  m2cpminvid2lem  22868  decpmatid  22884  decpmatmullem  22885  pmatcollpw2lem  22891  monmatcollpw  22893  pm2mpfval  22910  mp2pm2mplem4  22923  pm2mpmhmlem2  22933  chpmatval  22945  fcfval  24147  cnextfval  24176  utopsnneiplem  24361  rrxmvallem  25520  rrxmval  25521  itgpowd  26166  taylpval  26484  lgamgulmlem2  27148  lgamcvglem  27158  logexprlim  27343  dchr1  27375  ishlg  28825  mirval  28882  mirfv  28883  ishpg  28986  lmif  29033  islmib  29035  lmodvslmhm  33278  psgnfzto1stlem  33328  tocycfv  33337  sgnsval  33389  psrnzr  33814  0mplrim  33816  selvply1rhmlemb  33821  selvply1rhmlem2  33823  mplvrpmrhm  33849  esplyfval0  33866  esplyind  33877  evls1fldgencl  33972  minplyval  34007  rtelextdg2lem  34028  2sqr3minply  34082  cos9thpiminply  34090  zarcls0  34170  zarcls1  34171  zarclsiin  34173  zarclsint  34174  zarclssn  34175  qqhvval  34285  esummulc1  34383  esumcvg  34388  ofcval  34401  sigagenval  34442  measinb  34523  omsfval  34596  omssubadd  34602  sitgfval  34643  eulerpartlemsv1  34658  eulerpartlems  34662  fibp1  34703  totprobd  34728  probmeasb  34732  dstrvprob  34774  dstfrvinc  34779  dstfrvclim1  34780  ballotlemfval  34792  ballotlemsv  34812  gsumnunsn  34843  signsply0  34850  signstfval  34863  fdvneggt  34899  fdvnegge  34901  itgexpif  34905  breprexplema  34929  vtsval  34936  logdivsqrle  34949  hgt750lemg  34953  afsval  34973  lpadval  34978  cvmliftlem9  35651  goel  35705  satf0suc  35734  sat1el2xp  35737  fmlafv  35738  fmla  35739  fmlasuc0  35742  ex-sategoelel  35779  ex-sategoelelomsuc  35784  mvrsval  35863  mrsubfval  35866  mrsubval  35867  msubfval  35882  msubval  35883  msrval  35896  fwddifval  36520  fwddifnval  36521  knoppcnlem1  36939  knoppcnlem4  36942  knoppcnlem6  36944  knoppcnlem7  36945  bj-imdirval2  37682  bj-iminvval2  37693  bj-fvmptunsn2  37757  bj-endval  37814  poimirlem1  38127  poimirlem2  38128  poimirlem5  38131  poimirlem6  38132  poimirlem7  38133  poimirlem10  38136  poimirlem11  38137  poimirlem12  38138  poimirlem19  38145  poimirlem22  38148  mblfinlem2  38164  areacirc  38219  tendopl2  41408  tendoi2  41426  erngplus2  41435  erngplus2-rN  41443  hlhilset  42565  rhmzrhval  42596  lcmineqlem12  42664  aks4d1p9  42712  primrootscoprbij  42726  aks6d1c1p3  42734  aks6d1c1p5  42736  aks6d1c1  42740  hashscontpow  42746  aks6d1c3  42747  aks6d1c4  42748  aks6d1c2lem4  42751  aks6d1c2  42754  aks6d1c5lem3  42761  deg1gprod  42764  sticksstones2  42771  sticksstones3  42772  sticksstones6  42775  sticksstones7  42776  sticksstones8  42777  sticksstones10  42779  sticksstones12a  42781  sticksstones12  42782  sticksstones17  42787  sticksstones18  42788  sticksstones19  42789  aks6d1c6lem1  42794  aks6d1c6lem2  42795  aks6d1c6lem3  42796  aks6d1c6lem4  42797  aks6d1c6isolem1  42798  aks6d1c6isolem2  42799  aks6d1c6isolem3  42800  aks6d1c6lem5  42801  aks6d1c7lem1  42804  aks5lem2  42811  aks5lem3a  42813  unitscyglem1  42819  rfovfvd  44585  rfovfvfvd  44586  rfovcnvf1od  44587  rfovcnvfvd  44590  fsovfvd  44593  fsovfvfvd  44594  fsovcnvlem  44596  dssmapfv2d  44601  dssmapfv3d  44602  dssmapnvod  44603  clsk3nimkb  44623  dvgrat  44881  radcnvrat  44883  hashnzfzclim  44891  binomcxplemnn0  44918  binomcxplemrat  44919  binomcxplemfrat  44920  binomcxplemradcnv  44921  binomcxplemcvg  44923  binomcxplemdvsum  44924  binomcxplemnotnn0  44925  mapss2  45781  fmuldfeqlem1  46157  clim1fr1  46176  climrec  46178  climexp  46180  climneg  46185  divcnvg  46202  sumnnodd  46205  supcnvlimsup  46313  icccncfext  46460  cncfioobdlem  46469  fprodsubrecnncnvlem  46480  fprodaddrecnncnvlem  46482  dvsinax  46486  fperdvper  46492  dvcosax  46499  ioodvbdlimc1lem2  46505  ioodvbdlimc2lem  46507  dvnmul  46516  dvnprodlem1  46519  dvnprodlem2  46520  dvnprodlem3  46521  itgsinexp  46528  itgcoscmulx  46542  itgsincmulx  46547  itgsubsticclem  46548  itgsubsticc  46549  itgiccshift  46553  wallispilem5  46642  wallispi  46643  wallispi2lem1  46644  wallispi2lem2  46645  wallispi2  46646  stirlinglem1  46647  stirlinglem2  46648  stirlinglem3  46649  stirlinglem4  46650  stirlinglem5  46651  stirlinglem7  46653  stirlinglem8  46654  stirlinglem10  46656  stirlinglem11  46657  stirlinglem12  46658  stirlinglem13  46659  stirlinglem14  46660  stirlinglem15  46661  dirkerval2  46667  dirkercncflem2  46677  fourierdlem7  46687  fourierdlem13  46693  fourierdlem14  46694  fourierdlem16  46696  fourierdlem18  46698  fourierdlem19  46699  fourierdlem21  46701  fourierdlem22  46702  fourierdlem26  46706  fourierdlem37  46717  fourierdlem39  46719  fourierdlem41  46721  fourierdlem50  46729  fourierdlem51  46730  fourierdlem53  46732  fourierdlem62  46741  fourierdlem63  46742  fourierdlem65  46744  fourierdlem73  46752  fourierdlem74  46753  fourierdlem75  46754  fourierdlem76  46755  fourierdlem79  46758  fourierdlem81  46760  fourierdlem82  46761  fourierdlem83  46762  fourierdlem84  46763  fourierdlem88  46767  fourierdlem89  46768  fourierdlem90  46769  fourierdlem91  46770  fourierdlem92  46771  fourierdlem93  46772  fourierdlem97  46776  fourierdlem101  46780  fourierdlem103  46782  fourierdlem104  46783  fourierdlem111  46790  fourierdlem112  46791  fouriersw  46804  elaa2lem  46806  etransclem13  46820  etransclem17  46824  etransclem18  46825  etransclem21  46828  etransclem31  46838  etransclem32  46839  etransclem33  46840  etransclem35  46842  etransclem46  46853  etransclem48  46855  rrxtopnfi  46860  salgenval  46894  sge0val  46939  sge0z  46948  sge0snmpt  46956  sge0xp  47002  nnfoctbdjlem  47028  omeiunltfirp  47092  caratheodorylem1  47099  0ome  47102  ovnval2  47118  hoicvr  47121  ovncvrrp  47137  ovn0lem  47138  ovnsubaddlem1  47143  hsphoif  47149  hsphoival  47152  hoidmv1le  47167  hoidmvlelem3  47170  ovnhoilem2  47175  ovncvr2  47184  hoidifhspval2  47188  hoidifhspval3  47192  hspmbllem2  47200  smfid  47325  fsetsnf1  47645  fsetsnfo  47646  cfsetsnfsetfv  47650  cfsetsnfsetfo  47653  fvmptrab  47885  fundcmpsurinjlem3  48005  sprval  48084  prproropreud  48114  upgrimwlklem3  48520  grtri  48561  stgrfv  48574  isubgr3stgrlem5  48591  rngcvalALTV  48886  rngcidALTV  48895  rhmsubcALTVlem3  48904  ringcvalALTV  48910  funcringcsetcALTV2lem1  48911  ringcidALTV  48929  funcringcsetclem1ALTV  48934  scmsuppss  49003  ply1mulgsum  49022  lindslinindsimp1  49089  lindsrng01  49100  islindeps2  49115  fdivmptfv  49177  refdivmptfv  49178  1arympt1fv  49271  itcoval0  49294  itcoval1  49295  itcoval2  49296  itcoval3  49297  itcovalsuc  49299  ackvalsuc1mpt  49310  ackvalsuc1  49311  ackval1  49313  ackval2  49314  ackval3  49315  ackval0val  49318  swapf1a  49899  swapf2a  49901  swapf1  49902  swapf2  49904  tposcurf2val  49931  fuco23  49971  prcof1  50018  prcof21a  50021  mndtcid  50219  amgmwlem  50432