Theorem fvmptd 7001

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146   ↦ cmpt 5194  ‘cfv 6540

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-iota 6496  df-fun 6542  df-fv 6548

This theorem is used by:  fvmptd2  7002  fvmptdv2  7012  fvmptd4  7018  mptcnfimad  7985  fsplitfpar  8115  mpocurryvald  8268  ttukeylem3  10506  indval  12232  indfval  12236  tpf1ofv0  14546  tpf1ofv1  14547  tpf1ofv2  14548  ccatval1  14627  ccatval2  14628  repswsymb  14830  relexp1g  15082  rtrclreclem1  15113  rtrclreclem4  15117  dfrtrcl2  15118  prmodvdslcmf  17124  prmgap  17136  prmgaplcm  17137  prmgapprmo  17139  prdsvscafval  17550  mrcval  17683  cidval  17750  subcid  17921  idfu2nd  17951  resf2nd  17969  fuccoval  18040  fucid  18048  homaval  18105  idaval  18132  setcid  18160  catcid  18181  estrcid  18207  funcestrcsetclem1  18213  funcsetcestrclem1  18227  prf1  18273  prf2  18275  curf1  18298  curf11  18299  curf2val  18303  hof2  18330  yonedalem4a  18348  vrmdval  18939  smndex1gbasOLD  18985  smndex1gid  18986  smndex1gidOLD  18987  smndex1n0mnd  18997  mulgnngsum  19168  pj1val  19788  dpjval  20151  c0mgm  20566  c0mhm  20567  c0snmgmhm  20569  c0snmhm  20570  zrrnghm  20664  zrinitorngc  20770  zrtermorngc  20771  zrtermoringc  20803  sraval  21325  rngqiprngimfv  21467  frlmphl  21960  opsrval  22226  selvfval  22299  mhpval  22331  mhpsclcl  22339  psdfval  22350  cply1mul  22485  cply1coe0  22490  cply1coe0bi  22491  gsummoncoe1  22497  evls1sca  22512  mvmulfv  22730  mavmulfv  22732  mdetuni0  22807  mat2pmatval  22910  m2cpm  22927  cpm2mval  22936  m2cpminvid2lem  22940  decpmatid  22956  decpmatmullem  22957  pmatcollpw2lem  22963  monmatcollpw  22965  pm2mpfval  22982  mp2pm2mplem4  22995  pm2mpmhmlem2  23005  chpmatval  23017  fcfval  24219  cnextfval  24248  utopsnneiplem  24433  rrxmvallem  25592  rrxmval  25593  itgpowd  26238  taylpval  26559  lgamgulmlem2  27223  lgamcvglem  27233  logexprlim  27418  dchr1  27450  ishlg  28903  mirval  28961  mirfv  28962  ishpg  29070  lmif  29123  islmib  29125  lmodvslmhm  33393  psgnfzto1stlem  33443  tocycfv  33452  sgnsval  33504  psrnzr  33925  0mplrim  33927  selvply1rhmlemb  33932  selvply1rhmlem2  33934  mplvrpmrhm  33960  esplyfval0  33977  esplyind  33988  evls1fldgencl  34083  minplyval  34118  rtelextdg2lem  34139  2sqr3minply  34193  cos9thpiminply  34201  zarcls0  34281  zarcls1  34282  zarclsiin  34284  zarclsint  34285  zarclssn  34286  qqhvval  34396  esummulc1  34494  esumcvg  34499  ofcval  34512  sigagenval  34554  measinb  34635  omsfval  34708  omssubadd  34714  sitgfval  34755  eulerpartlemsv1  34770  eulerpartlems  34774  fibp1  34815  totprobd  34840  probmeasb  34844  dstrvprob  34886  dstfrvinc  34891  dstfrvclim1  34892  ballotlemfval  34904  ballotlemsv  34924  gsumnunsn  34955  signsply0  34962  signstfval  34975  fdvneggt  35011  fdvnegge  35013  itgexpif  35017  breprexplema  35041  vtsval  35048  logdivsqrle  35061  hgt750lemg  35065  afsval  35085  lpadval  35090  cvmliftlem9  35798  goel  35852  satf0suc  35881  sat1el2xp  35884  fmlafv  35885  fmla  35886  fmlasuc0  35889  ex-sategoelel  35926  ex-sategoelelomsuc  35931  mvrsval  36010  mrsubfval  36013  mrsubval  36014  msubfval  36029  msubval  36030  msrval  36043  fwddifval  36667  fwddifnval  36668  knoppcnlem1  37115  knoppcnlem4  37118  knoppcnlem6  37120  knoppcnlem7  37121  bj-imdirval2  37860  bj-iminvval2  37871  bj-fvmptunsn2  37935  bj-endval  37992  poimirlem1  38305  poimirlem2  38306  poimirlem5  38309  poimirlem6  38310  poimirlem7  38311  poimirlem10  38314  poimirlem11  38315  poimirlem12  38316  poimirlem19  38323  poimirlem22  38326  mblfinlem2  38342  areacirc  38397  tendopl2  41584  tendoi2  41602  erngplus2  41611  erngplus2-rN  41619  hlhilset  42741  rhmzrhval  42772  lcmineqlem12  42840  aks4d1p9  42888  primrootscoprbij  42902  aks6d1c1p3  42910  aks6d1c1p5  42912  aks6d1c1  42916  hashscontpow  42922  aks6d1c3  42923  aks6d1c4  42924  aks6d1c2lem4  42927  aks6d1c2  42930  aks6d1c5lem3  42937  deg1gprod  42940  sticksstones2  42947  sticksstones3  42948  sticksstones6  42951  sticksstones7  42952  sticksstones8  42953  sticksstones10  42955  sticksstones12a  42957  sticksstones12  42958  sticksstones17  42963  sticksstones18  42964  sticksstones19  42965  aks6d1c6lem1  42970  aks6d1c6lem2  42971  aks6d1c6lem3  42972  aks6d1c6lem4  42973  aks6d1c6isolem1  42974  aks6d1c6isolem2  42975  aks6d1c6isolem3  42976  aks6d1c6lem5  42977  aks6d1c7lem1  42980  aks5lem2  42987  aks5lem3a  42989  unitscyglem1  42995  rfovfvd  44761  rfovfvfvd  44762  rfovcnvf1od  44763  rfovcnvfvd  44766  fsovfvd  44769  fsovfvfvd  44770  fsovcnvlem  44772  dssmapfv2d  44777  dssmapfv3d  44778  dssmapnvod  44779  clsk3nimkb  44799  dvgrat  45055  radcnvrat  45057  hashnzfzclim  45065  binomcxplemnn0  45092  binomcxplemrat  45093  binomcxplemfrat  45094  binomcxplemradcnv  45095  binomcxplemcvg  45097  binomcxplemdvsum  45098  binomcxplemnotnn0  45099  mapss2  45955  fmuldfeqlem1  46331  clim1fr1  46350  climrec  46352  climexp  46354  climneg  46359  divcnvg  46376  sumnnodd  46379  supcnvlimsup  46487  icccncfext  46634  cncfioobdlem  46643  fprodsubrecnncnvlem  46654  fprodaddrecnncnvlem  46656  dvsinax  46660  fperdvper  46666  dvcosax  46673  ioodvbdlimc1lem2  46679  ioodvbdlimc2lem  46681  dvnmul  46690  dvnprodlem1  46693  dvnprodlem2  46694  dvnprodlem3  46695  itgsinexp  46702  itgcoscmulx  46716  itgsincmulx  46721  itgsubsticclem  46722  itgsubsticc  46723  itgiccshift  46727  wallispilem5  46816  wallispi  46817  wallispi2lem1  46818  wallispi2lem2  46819  wallispi2  46820  stirlinglem1  46821  stirlinglem2  46822  stirlinglem3  46823  stirlinglem4  46824  stirlinglem5  46825  stirlinglem7  46827  stirlinglem8  46828  stirlinglem10  46830  stirlinglem11  46831  stirlinglem12  46832  stirlinglem13  46833  stirlinglem14  46834  stirlinglem15  46835  dirkerval2  46841  dirkercncflem2  46851  fourierdlem7  46861  fourierdlem13  46867  fourierdlem14  46868  fourierdlem16  46870  fourierdlem18  46872  fourierdlem19  46873  fourierdlem21  46875  fourierdlem22  46876  fourierdlem26  46880  fourierdlem37  46891  fourierdlem39  46893  fourierdlem41  46895  fourierdlem50  46903  fourierdlem51  46904  fourierdlem53  46906  fourierdlem62  46915  fourierdlem63  46916  fourierdlem65  46918  fourierdlem73  46926  fourierdlem74  46927  fourierdlem75  46928  fourierdlem76  46929  fourierdlem79  46932  fourierdlem81  46934  fourierdlem82  46935  fourierdlem83  46936  fourierdlem84  46937  fourierdlem88  46941  fourierdlem89  46942  fourierdlem90  46943  fourierdlem91  46944  fourierdlem92  46945  fourierdlem93  46946  fourierdlem97  46950  fourierdlem101  46954  fourierdlem103  46956  fourierdlem104  46957  fourierdlem111  46964  fourierdlem112  46965  fouriersw  46978  elaa2lem  46980  etransclem13  46994  etransclem17  46998  etransclem18  46999  etransclem21  47002  etransclem31  47012  etransclem32  47013  etransclem33  47014  etransclem35  47016  etransclem46  47027  etransclem48  47029  rrxtopnfi  47034  salgenval  47068  sge0val  47113  sge0z  47122  sge0snmpt  47130  sge0xp  47176  nnfoctbdjlem  47202  omeiunltfirp  47266  caratheodorylem1  47273  0ome  47276  ovnval2  47292  hoicvr  47295  ovncvrrp  47311  ovn0lem  47312  ovnsubaddlem1  47317  hsphoif  47323  hsphoival  47326  hoidmv1le  47341  hoidmvlelem3  47344  ovnhoilem2  47349  ovncvr2  47358  hoidifhspval2  47362  hoidifhspval3  47366  hspmbllem2  47374  smfid  47499  fsetsnf1  47822  fsetsnfo  47823  cfsetsnfsetfv  47827  cfsetsnfsetfo  47830  fvmptrab  48062  fundcmpsurinjlem3  48182  sprval  48261  prproropreud  48291  upgrimwlklem3  48697  grtri  48738  stgrfv  48751  isubgr3stgrlem5  48768  rngcvalALTV  49063  rngcidALTV  49072  rhmsubcALTVlem3  49081  ringcvalALTV  49087  funcringcsetcALTV2lem1  49088  ringcidALTV  49106  funcringcsetclem1ALTV  49111  scmsuppss  49184  ply1mulgsum  49203  lindslinindsimp1  49270  lindsrng01  49281  islindeps2  49296  fdivmptfv  49358  refdivmptfv  49359  1arympt1fv  49452  itcoval0  49475  itcoval1  49476  itcoval2  49477  itcoval3  49478  itcovalsuc  49480  ackvalsuc1mpt  49491  ackvalsuc1  49492  ackval1  49494  ackval2  49495  ackval3  49496  ackval0val  49499  swapf1a  50080  swapf2a  50082  swapf1  50083  swapf2  50085  tposcurf2val  50112  fuco23  50152  prcof1  50199  prcof21a  50202  mndtcid  50400  amgmwlem  50683