Theorem fvmptd 6992

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108   ↦ cmpt 5201  ‘cfv 6530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-iota 6483  df-fun 6532  df-fv 6538

This theorem is referenced by:  fvmptd2  6993  fvmptdv2  7003  fvmptd4  7009  mptcnfimad  7983  fsplitfpar  8115  mpocurryvald  8267  ttukeylem3  10523  tpf1ofv0  14512  tpf1ofv1  14513  tpf1ofv2  14514  ccatval1  14593  ccatval2  14594  repswsymb  14790  relexp1g  15043  rtrclreclem1  15074  rtrclreclem4  15078  dfrtrcl2  15079  prmodvdslcmf  17065  prmgap  17077  prmgaplcm  17078  prmgapprmo  17080  prdsvscafval  17492  mrcval  17620  cidval  17687  subcid  17858  idfu2nd  17888  resf2nd  17906  fuccoval  17977  fucid  17985  homaval  18042  idaval  18069  setcid  18097  catcid  18118  estrcid  18144  funcestrcsetclem1  18150  funcsetcestrclem1  18164  prf1  18210  prf2  18212  curf1  18235  curf11  18236  curf2val  18240  hof2  18267  yonedalem4a  18285  vrmdval  18833  smndex1gbas  18878  smndex1gid  18879  smndex1n0mnd  18888  mulgnngsum  19060  pj1val  19674  dpjval  20037  c0mgm  20417  c0mhm  20418  c0snmgmhm  20420  c0snmhm  20421  zrrnghm  20494  zrinitorngc  20600  zrtermorngc  20601  zrtermoringc  20633  sraval  21131  rngqiprngimfv  21257  frlmphl  21739  opsrval  22002  selvfval  22070  mhpval  22075  mhpsclcl  22083  psdfval  22094  cply1mul  22232  cply1coe0  22237  cply1coe0bi  22238  gsummoncoe1  22244  evls1sca  22259  mvmulfv  22480  mavmulfv  22482  mdetuni0  22557  mat2pmatval  22660  m2cpm  22677  cpm2mval  22686  m2cpminvid2lem  22690  decpmatid  22706  decpmatmullem  22707  pmatcollpw2lem  22713  monmatcollpw  22715  pm2mpfval  22732  mp2pm2mplem4  22745  pm2mpmhmlem2  22755  chpmatval  22767  fcfval  23969  cnextfval  23998  utopsnneiplem  24184  rrxmvallem  25354  rrxmval  25355  itgpowd  26007  taylpval  26324  lgamgulmlem2  26990  lgamcvglem  27000  logexprlim  27186  dchr1  27218  ishlg  28527  mirval  28580  mirfv  28581  ishpg  28684  lmif  28710  islmib  28712  indval  32776  indfval  32779  lmodvslmhm  32990  psgnfzto1stlem  33057  tocycfv  33066  sgnsval  33118  evls1fldgencl  33657  minplyval  33685  rtelextdg2lem  33706  2sqr3minply  33760  cos9thpiminply  33768  zarcls0  33845  zarcls1  33846  zarclsiin  33848  zarclsint  33849  zarclssn  33850  qqhvval  33960  esummulc1  34058  esumcvg  34063  ofcval  34076  sigagenval  34117  measinb  34198  omsfval  34272  omssubadd  34278  sitgfval  34319  eulerpartlemsv1  34334  eulerpartlems  34338  fibp1  34379  totprobd  34404  probmeasb  34408  dstrvprob  34450  dstfrvinc  34455  dstfrvclim1  34456  ballotlemfval  34468  ballotlemsv  34488  gsumnunsn  34519  signsply0  34529  signstfval  34542  fdvneggt  34578  fdvnegge  34580  itgexpif  34584  breprexplema  34608  vtsval  34615  logdivsqrle  34628  hgt750lemg  34632  afsval  34649  lpadval  34654  cvmliftlem9  35261  goel  35315  satf0suc  35344  sat1el2xp  35347  fmlafv  35348  fmla  35349  fmlasuc0  35352  ex-sategoelel  35389  ex-sategoelelomsuc  35394  mvrsval  35473  mrsubfval  35476  mrsubval  35477  msubfval  35492  msubval  35493  msrval  35506  fwddifval  36126  fwddifnval  36127  knoppcnlem1  36457  knoppcnlem4  36460  knoppcnlem6  36462  knoppcnlem7  36463  bj-imdirval2  37147  bj-iminvval2  37158  bj-fvmptunsn2  37222  bj-endval  37279  poimirlem1  37591  poimirlem2  37592  poimirlem5  37595  poimirlem6  37596  poimirlem7  37597  poimirlem10  37600  poimirlem11  37601  poimirlem12  37602  poimirlem19  37609  poimirlem22  37612  mblfinlem2  37628  areacirc  37683  tendopl2  40742  tendoi2  40760  erngplus2  40769  erngplus2-rN  40777  hlhilset  41899  rhmzrhval  41930  lcmineqlem12  41999  aks4d1p9  42047  primrootscoprbij  42061  aks6d1c1p3  42069  aks6d1c1p5  42071  aks6d1c1  42075  hashscontpow  42081  aks6d1c3  42082  aks6d1c4  42083  aks6d1c2lem4  42086  aks6d1c2  42089  aks6d1c5lem3  42096  deg1gprod  42099  sticksstones2  42106  sticksstones3  42107  sticksstones6  42110  sticksstones7  42111  sticksstones8  42112  sticksstones10  42114  sticksstones12a  42116  sticksstones12  42117  sticksstones17  42122  sticksstones18  42123  sticksstones19  42124  aks6d1c6lem1  42129  aks6d1c6lem2  42130  aks6d1c6lem3  42131  aks6d1c6lem4  42132  aks6d1c6isolem1  42133  aks6d1c6isolem2  42134  aks6d1c6isolem3  42135  aks6d1c6lem5  42136  aks6d1c7lem1  42139  aks5lem2  42146  aks5lem3a  42148  unitscyglem1  42154  metakunt3  42166  metakunt4  42167  metakunt5  42168  metakunt6  42169  metakunt7  42170  metakunt8  42171  metakunt10  42173  metakunt11  42174  metakunt12  42175  metakunt20  42183  metakunt21  42184  metakunt22  42185  metakunt26  42189  metakunt27  42190  metakunt28  42191  metakunt29  42192  metakunt30  42193  metakunt32  42195  rfovfvd  43973  rfovfvfvd  43974  rfovcnvf1od  43975  rfovcnvfvd  43978  fsovfvd  43981  fsovfvfvd  43982  fsovcnvlem  43984  dssmapfv2d  43989  dssmapfv3d  43990  dssmapnvod  43991  clsk3nimkb  44011  dvgrat  44284  radcnvrat  44286  hashnzfzclim  44294  binomcxplemnn0  44321  binomcxplemrat  44322  binomcxplemfrat  44323  binomcxplemradcnv  44324  binomcxplemcvg  44326  binomcxplemdvsum  44327  binomcxplemnotnn0  44328  mapss2  45177  fmuldfeqlem1  45559  clim1fr1  45578  climrec  45580  climexp  45582  climneg  45587  divcnvg  45604  sumnnodd  45607  supcnvlimsup  45717  icccncfext  45864  cncfioobdlem  45873  fprodsubrecnncnvlem  45884  fprodaddrecnncnvlem  45886  dvsinax  45890  fperdvper  45896  dvcosax  45903  ioodvbdlimc1lem2  45909  ioodvbdlimc2lem  45911  dvnmul  45920  dvnprodlem1  45923  dvnprodlem2  45924  dvnprodlem3  45925  itgsinexp  45932  itgcoscmulx  45946  itgsincmulx  45951  itgsubsticclem  45952  itgsubsticc  45953  itgiccshift  45957  wallispilem5  46046  wallispi  46047  wallispi2lem1  46048  wallispi2lem2  46049  wallispi2  46050  stirlinglem1  46051  stirlinglem2  46052  stirlinglem3  46053  stirlinglem4  46054  stirlinglem5  46055  stirlinglem7  46057  stirlinglem8  46058  stirlinglem10  46060  stirlinglem11  46061  stirlinglem12  46062  stirlinglem13  46063  stirlinglem14  46064  stirlinglem15  46065  dirkerval2  46071  dirkercncflem2  46081  fourierdlem7  46091  fourierdlem13  46097  fourierdlem14  46098  fourierdlem16  46100  fourierdlem18  46102  fourierdlem19  46103  fourierdlem21  46105  fourierdlem22  46106  fourierdlem26  46110  fourierdlem37  46121  fourierdlem39  46123  fourierdlem41  46125  fourierdlem48  46131  fourierdlem49  46132  fourierdlem50  46133  fourierdlem51  46134  fourierdlem53  46136  fourierdlem62  46145  fourierdlem63  46146  fourierdlem65  46148  fourierdlem73  46156  fourierdlem74  46157  fourierdlem75  46158  fourierdlem76  46159  fourierdlem79  46162  fourierdlem81  46164  fourierdlem82  46165  fourierdlem83  46166  fourierdlem84  46167  fourierdlem88  46171  fourierdlem89  46172  fourierdlem90  46173  fourierdlem91  46174  fourierdlem92  46175  fourierdlem93  46176  fourierdlem97  46180  fourierdlem101  46184  fourierdlem103  46186  fourierdlem104  46187  fourierdlem111  46194  fourierdlem112  46195  fouriersw  46208  elaa2lem  46210  etransclem13  46224  etransclem17  46228  etransclem18  46229  etransclem21  46232  etransclem31  46242  etransclem32  46243  etransclem33  46244  etransclem35  46246  etransclem46  46257  etransclem48  46259  rrxtopnfi  46264  salgenval  46298  sge0val  46343  sge0z  46352  sge0snmpt  46360  sge0xp  46406  nnfoctbdjlem  46432  omeiunltfirp  46496  caratheodorylem1  46503  0ome  46506  ovnval2  46522  hoicvr  46525  ovncvrrp  46541  ovn0lem  46542  ovnsubaddlem1  46547  hsphoif  46553  hsphoival  46556  hoidmv1le  46571  hoidmvlelem3  46574  ovnhoilem2  46579  ovncvr2  46588  hoidifhspval2  46592  hoidifhspval3  46596  hspmbllem2  46604  smfid  46729  fsetsnf1  47029  fsetsnfo  47030  cfsetsnfsetfv  47034  cfsetsnfsetfo  47037  fvmptrab  47269  fundcmpsurinjlem3  47362  sprval  47441  prproropreud  47471  upgrimwlklem3  47860  grtri  47900  stgrfv  47913  isubgr3stgrlem5  47930  rngcvalALTV  48188  rngcidALTV  48197  rhmsubcALTVlem3  48206  ringcvalALTV  48212  funcringcsetcALTV2lem1  48213  ringcidALTV  48231  funcringcsetclem1ALTV  48236  scmsuppss  48294  ply1mulgsum  48314  lindslinindsimp1  48381  lindsrng01  48392  islindeps2  48407  fdivmptfv  48473  refdivmptfv  48474  1arympt1fv  48567  itcoval0  48590  itcoval1  48591  itcoval2  48592  itcoval3  48593  itcovalsuc  48595  ackvalsuc1mpt  48606  ackvalsuc1  48607  ackval1  48609  ackval2  48610  ackval3  48611  ackval0val  48614  swapf1a  49134  swapf2a  49136  swapf1  49137  swapf2  49139  tposcurf2val  49160  fuco23  49200  prcof1  49246  prcof21a  49249  mndtcid  49414  amgmwlem  49614