Theorem fvmptd 6936

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2111   ↦ cmpt 5172  ‘cfv 6481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-mpt 5173  df-id 5511  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-iota 6437  df-fun 6483  df-fv 6489

This theorem is referenced by:  fvmptd2  6937  fvmptdv2  6947  fvmptd4  6953  mptcnfimad  7918  fsplitfpar  8048  mpocurryvald  8200  ttukeylem3  10402  tpf1ofv0  14403  tpf1ofv1  14404  tpf1ofv2  14405  ccatval1  14484  ccatval2  14485  repswsymb  14681  relexp1g  14933  rtrclreclem1  14964  rtrclreclem4  14968  dfrtrcl2  14969  prmodvdslcmf  16959  prmgap  16971  prmgaplcm  16972  prmgapprmo  16974  prdsvscafval  17384  mrcval  17516  cidval  17583  subcid  17754  idfu2nd  17784  resf2nd  17802  fuccoval  17873  fucid  17881  homaval  17938  idaval  17965  setcid  17993  catcid  18014  estrcid  18040  funcestrcsetclem1  18046  funcsetcestrclem1  18060  prf1  18106  prf2  18108  curf1  18131  curf11  18132  curf2val  18136  hof2  18163  yonedalem4a  18181  vrmdval  18765  smndex1gbas  18810  smndex1gid  18811  smndex1n0mnd  18820  mulgnngsum  18992  pj1val  19608  dpjval  19971  c0mgm  20378  c0mhm  20379  c0snmgmhm  20381  c0snmhm  20382  zrrnghm  20452  zrinitorngc  20558  zrtermorngc  20559  zrtermoringc  20591  sraval  21110  rngqiprngimfv  21236  frlmphl  21719  opsrval  21982  selvfval  22050  mhpval  22055  mhpsclcl  22063  psdfval  22074  cply1mul  22212  cply1coe0  22217  cply1coe0bi  22218  gsummoncoe1  22224  evls1sca  22239  mvmulfv  22460  mavmulfv  22462  mdetuni0  22537  mat2pmatval  22640  m2cpm  22657  cpm2mval  22666  m2cpminvid2lem  22670  decpmatid  22686  decpmatmullem  22687  pmatcollpw2lem  22693  monmatcollpw  22695  pm2mpfval  22712  mp2pm2mplem4  22725  pm2mpmhmlem2  22735  chpmatval  22747  fcfval  23949  cnextfval  23978  utopsnneiplem  24163  rrxmvallem  25332  rrxmval  25333  itgpowd  25985  taylpval  26302  lgamgulmlem2  26968  lgamcvglem  26978  logexprlim  27164  dchr1  27196  ishlg  28581  mirval  28634  mirfv  28635  ishpg  28738  lmif  28764  islmib  28766  indval  32832  indfval  32835  lmodvslmhm  33028  psgnfzto1stlem  33067  tocycfv  33076  sgnsval  33128  mplvrpmrhm  33575  evls1fldgencl  33681  minplyval  33716  rtelextdg2lem  33737  2sqr3minply  33791  cos9thpiminply  33799  zarcls0  33879  zarcls1  33880  zarclsiin  33882  zarclsint  33883  zarclssn  33884  qqhvval  33994  esummulc1  34092  esumcvg  34097  ofcval  34110  sigagenval  34151  measinb  34232  omsfval  34305  omssubadd  34311  sitgfval  34352  eulerpartlemsv1  34367  eulerpartlems  34371  fibp1  34412  totprobd  34437  probmeasb  34441  dstrvprob  34483  dstfrvinc  34488  dstfrvclim1  34489  ballotlemfval  34501  ballotlemsv  34521  gsumnunsn  34552  signsply0  34562  signstfval  34575  fdvneggt  34611  fdvnegge  34613  itgexpif  34617  breprexplema  34641  vtsval  34648  logdivsqrle  34661  hgt750lemg  34665  afsval  34682  lpadval  34687  cvmliftlem9  35335  goel  35389  satf0suc  35418  sat1el2xp  35421  fmlafv  35422  fmla  35423  fmlasuc0  35426  ex-sategoelel  35463  ex-sategoelelomsuc  35468  mvrsval  35547  mrsubfval  35550  mrsubval  35551  msubfval  35566  msubval  35567  msrval  35580  fwddifval  36202  fwddifnval  36203  knoppcnlem1  36533  knoppcnlem4  36536  knoppcnlem6  36538  knoppcnlem7  36539  bj-imdirval2  37223  bj-iminvval2  37234  bj-fvmptunsn2  37298  bj-endval  37355  poimirlem1  37667  poimirlem2  37668  poimirlem5  37671  poimirlem6  37672  poimirlem7  37673  poimirlem10  37676  poimirlem11  37677  poimirlem12  37678  poimirlem19  37685  poimirlem22  37688  mblfinlem2  37704  areacirc  37759  tendopl2  40822  tendoi2  40840  erngplus2  40849  erngplus2-rN  40857  hlhilset  41979  rhmzrhval  42010  lcmineqlem12  42079  aks4d1p9  42127  primrootscoprbij  42141  aks6d1c1p3  42149  aks6d1c1p5  42151  aks6d1c1  42155  hashscontpow  42161  aks6d1c3  42162  aks6d1c4  42163  aks6d1c2lem4  42166  aks6d1c2  42169  aks6d1c5lem3  42176  deg1gprod  42179  sticksstones2  42186  sticksstones3  42187  sticksstones6  42190  sticksstones7  42191  sticksstones8  42192  sticksstones10  42194  sticksstones12a  42196  sticksstones12  42197  sticksstones17  42202  sticksstones18  42203  sticksstones19  42204  aks6d1c6lem1  42209  aks6d1c6lem2  42210  aks6d1c6lem3  42211  aks6d1c6lem4  42212  aks6d1c6isolem1  42213  aks6d1c6isolem2  42214  aks6d1c6isolem3  42215  aks6d1c6lem5  42216  aks6d1c7lem1  42219  aks5lem2  42226  aks5lem3a  42228  unitscyglem1  42234  rfovfvd  44041  rfovfvfvd  44042  rfovcnvf1od  44043  rfovcnvfvd  44046  fsovfvd  44049  fsovfvfvd  44050  fsovcnvlem  44052  dssmapfv2d  44057  dssmapfv3d  44058  dssmapnvod  44059  clsk3nimkb  44079  dvgrat  44351  radcnvrat  44353  hashnzfzclim  44361  binomcxplemnn0  44388  binomcxplemrat  44389  binomcxplemfrat  44390  binomcxplemradcnv  44391  binomcxplemcvg  44393  binomcxplemdvsum  44394  binomcxplemnotnn0  44395  mapss2  45248  fmuldfeqlem1  45628  clim1fr1  45647  climrec  45649  climexp  45651  climneg  45656  divcnvg  45673  sumnnodd  45676  supcnvlimsup  45784  icccncfext  45931  cncfioobdlem  45940  fprodsubrecnncnvlem  45951  fprodaddrecnncnvlem  45953  dvsinax  45957  fperdvper  45963  dvcosax  45970  ioodvbdlimc1lem2  45976  ioodvbdlimc2lem  45978  dvnmul  45987  dvnprodlem1  45990  dvnprodlem2  45991  dvnprodlem3  45992  itgsinexp  45999  itgcoscmulx  46013  itgsincmulx  46018  itgsubsticclem  46019  itgsubsticc  46020  itgiccshift  46024  wallispilem5  46113  wallispi  46114  wallispi2lem1  46115  wallispi2lem2  46116  wallispi2  46117  stirlinglem1  46118  stirlinglem2  46119  stirlinglem3  46120  stirlinglem4  46121  stirlinglem5  46122  stirlinglem7  46124  stirlinglem8  46125  stirlinglem10  46127  stirlinglem11  46128  stirlinglem12  46129  stirlinglem13  46130  stirlinglem14  46131  stirlinglem15  46132  dirkerval2  46138  dirkercncflem2  46148  fourierdlem7  46158  fourierdlem13  46164  fourierdlem14  46165  fourierdlem16  46167  fourierdlem18  46169  fourierdlem19  46170  fourierdlem21  46172  fourierdlem22  46173  fourierdlem26  46177  fourierdlem37  46188  fourierdlem39  46190  fourierdlem41  46192  fourierdlem48  46198  fourierdlem49  46199  fourierdlem50  46200  fourierdlem51  46201  fourierdlem53  46203  fourierdlem62  46212  fourierdlem63  46213  fourierdlem65  46215  fourierdlem73  46223  fourierdlem74  46224  fourierdlem75  46225  fourierdlem76  46226  fourierdlem79  46229  fourierdlem81  46231  fourierdlem82  46232  fourierdlem83  46233  fourierdlem84  46234  fourierdlem88  46238  fourierdlem89  46239  fourierdlem90  46240  fourierdlem91  46241  fourierdlem92  46242  fourierdlem93  46243  fourierdlem97  46247  fourierdlem101  46251  fourierdlem103  46253  fourierdlem104  46254  fourierdlem111  46261  fourierdlem112  46262  fouriersw  46275  elaa2lem  46277  etransclem13  46291  etransclem17  46295  etransclem18  46296  etransclem21  46299  etransclem31  46309  etransclem32  46310  etransclem33  46311  etransclem35  46313  etransclem46  46324  etransclem48  46326  rrxtopnfi  46331  salgenval  46365  sge0val  46410  sge0z  46419  sge0snmpt  46427  sge0xp  46473  nnfoctbdjlem  46499  omeiunltfirp  46563  caratheodorylem1  46570  0ome  46573  ovnval2  46589  hoicvr  46592  ovncvrrp  46608  ovn0lem  46609  ovnsubaddlem1  46614  hsphoif  46620  hsphoival  46623  hoidmv1le  46638  hoidmvlelem3  46641  ovnhoilem2  46646  ovncvr2  46655  hoidifhspval2  46659  hoidifhspval3  46663  hspmbllem2  46671  smfid  46796  fsetsnf1  47089  fsetsnfo  47090  cfsetsnfsetfv  47094  cfsetsnfsetfo  47097  fvmptrab  47329  fundcmpsurinjlem3  47437  sprval  47516  prproropreud  47546  upgrimwlklem3  47936  grtri  47977  stgrfv  47990  isubgr3stgrlem5  48007  rngcvalALTV  48302  rngcidALTV  48311  rhmsubcALTVlem3  48320  ringcvalALTV  48326  funcringcsetcALTV2lem1  48327  ringcidALTV  48345  funcringcsetclem1ALTV  48350  scmsuppss  48408  ply1mulgsum  48428  lindslinindsimp1  48495  lindsrng01  48506  islindeps2  48521  fdivmptfv  48583  refdivmptfv  48584  1arympt1fv  48677  itcoval0  48700  itcoval1  48701  itcoval2  48702  itcoval3  48703  itcovalsuc  48705  ackvalsuc1mpt  48716  ackvalsuc1  48717  ackval1  48719  ackval2  48720  ackval3  48721  ackval0val  48724  swapf1a  49307  swapf2a  49309  swapf1  49310  swapf2  49312  tposcurf2val  49339  fuco23  49379  prcof1  49426  prcof21a  49429  mndtcid  49627  amgmwlem  49840