Theorem fvmptd 6994

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145   ↦ cmpt 5186  ‘cfv 6533

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-pr 5398

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-iota 6489  df-fun 6535  df-fv 6541

This theorem is used by:  fvmptd2  6995  fvmptdv2  7005  fvmptd4  7011  mptcnfimad  7983  fsplitfpar  8115  mpocurryvald  8268  ttukeylem3  10513  indval  12245  indfval  12249  tpf1ofv0  14561  tpf1ofv1  14562  tpf1ofv2  14563  ccatval1  14642  ccatval2  14643  repswsymb  14845  relexp1g  15099  rtrclreclem1  15130  rtrclreclem4  15134  dfrtrcl2  15135  prmodvdslcmf  17139  prmgap  17151  prmgaplcm  17152  prmgapprmo  17154  prdsvscafval  17565  mrcval  17698  cidval  17765  subcid  17936  idfu2nd  17966  resf2nd  17984  fuccoval  18055  fucid  18063  homaval  18120  idaval  18147  setcid  18175  catcid  18196  estrcid  18222  funcestrcsetclem1  18228  funcsetcestrclem1  18242  prf1  18288  prf2  18290  curf1  18313  curf11  18314  curf2val  18318  hof2  18345  yonedalem4a  18363  vrmdval  18966  smndex1gbasOLD  19012  smndex1gid  19013  smndex1gidOLD  19014  smndex1n0mnd  19024  mulgnngsum  19202  pj1val  19822  dpjval  20185  c0mgm  20600  c0mhm  20601  c0snmgmhm  20603  c0snmhm  20604  zrrnghm  20698  zrinitorngc  20804  zrtermorngc  20805  zrtermoringc  20837  sraval  21359  rngqiprngimfv  21501  frlmphl  21994  opsrval  22262  selvfval  22335  mhpval  22367  mhpsclcl  22375  psdfval  22386  cply1mul  22521  cply1coe0  22526  cply1coe0bi  22527  gsummoncoe1  22533  evls1sca  22548  mvmulfv  22766  mavmulfv  22768  mdetuni0  22843  mat2pmatval  22949  m2cpm  22966  cpm2mval  22975  m2cpminvid2lem  22979  decpmatid  22995  decpmatmullem  22996  pmatcollpw2lem  23002  monmatcollpw  23004  pm2mpfval  23021  mp2pm2mplem4  23034  pm2mpmhmlem2  23044  chpmatval  23056  fcfval  24259  cnextfval  24288  utopsnneiplem  24473  rrxmvallem  25632  rrxmval  25633  itgpowd  26277  taylpval  26603  lgamgulmlem2  27266  lgamcvglem  27276  logexprlim  27461  dchr1  27493  ishlg  28947  mirval  29006  mirfv  29007  ishpg  29116  lmif  29169  islmib  29171  lmodvslmhm  33490  psgnfzto1stlem  33540  tocycfv  33549  sgnsval  33601  psrnzr  34022  0mplrim  34024  selvply1rhmlemb  34029  selvply1rhmlem2  34031  mplvrpmrhm  34057  esplyfval0  34074  esplyind  34085  evls1fldgencl  34180  minplyval  34215  rtelextdg2lem  34236  2sqr3minply  34290  cos9thpiminply  34298  zarcls0  34378  zarcls1  34379  zarclsiin  34381  zarclsint  34382  zarclssn  34383  qqhvval  34493  esummulc1  34591  esumcvg  34596  ofcval  34609  sigagenval  34651  measinb  34732  omsfval  34805  omssubadd  34811  sitgfval  34852  eulerpartlemsv1  34867  eulerpartlems  34871  fibp1  34912  totprobd  34937  probmeasb  34941  dstrvprob  34983  dstfrvinc  34988  dstfrvclim1  34989  ballotlemfval  35001  ballotlemsv  35021  gsumnunsn  35052  signsply0  35059  signstfval  35072  fdvneggt  35108  fdvnegge  35110  itgexpif  35114  breprexplema  35138  vtsval  35145  logdivsqrle  35158  hgt750lemg  35162  afsval  35182  lpadval  35187  cvmliftlem9  35872  goel  35926  satf0suc  35955  sat1el2xp  35958  fmlafv  35959  fmla  35960  fmlasuc0  35963  ex-sategoelel  36000  ex-sategoelelomsuc  36005  mvrsval  36084  mrsubfval  36087  mrsubval  36088  msubfval  36103  msubval  36104  msrval  36117  fwddifval  36742  fwddifnval  36743  knoppcnlem1  37190  knoppcnlem4  37193  knoppcnlem6  37195  knoppcnlem7  37196  bj-imdirval2  37935  bj-iminvval2  37946  bj-fvmptunsn2  38010  bj-endval  38067  poimirlem1  38370  poimirlem2  38371  poimirlem5  38374  poimirlem6  38375  poimirlem7  38376  poimirlem10  38379  poimirlem11  38380  poimirlem12  38381  poimirlem19  38388  poimirlem22  38391  mblfinlem2  38407  areacirc  38462  tendopl2  41650  tendoi2  41668  erngplus2  41677  erngplus2-rN  41685  hlhilset  42807  rhmzrhval  42838  lcmineqlem12  42906  aks4d1p9  42954  primrootscoprbij  42968  aks6d1c1p3  42976  aks6d1c1p5  42978  aks6d1c1  42982  hashscontpow  42988  aks6d1c3  42989  aks6d1c4  42990  aks6d1c2lem4  42993  aks6d1c2  42996  aks6d1c5lem3  43003  deg1gprod  43006  sticksstones2  43013  sticksstones3  43014  sticksstones6  43017  sticksstones7  43018  sticksstones8  43019  sticksstones10  43021  sticksstones12a  43023  sticksstones12  43024  sticksstones17  43029  sticksstones18  43030  sticksstones19  43031  aks6d1c6lem1  43036  aks6d1c6lem2  43037  aks6d1c6lem3  43038  aks6d1c6lem4  43039  aks6d1c6isolem1  43040  aks6d1c6isolem2  43041  aks6d1c6isolem3  43042  aks6d1c6lem5  43043  aks6d1c7lem1  43046  aks5lem2  43053  aks5lem3a  43055  unitscyglem1  43061  rfovfvd  44842  rfovfvfvd  44843  rfovcnvf1od  44844  rfovcnvfvd  44847  fsovfvd  44850  fsovfvfvd  44851  fsovcnvlem  44853  dssmapfv2d  44858  dssmapfv3d  44859  dssmapnvod  44860  clsk3nimkb  44880  dvgrat  45136  radcnvrat  45138  hashnzfzclim  45146  binomcxplemnn0  45173  binomcxplemrat  45174  binomcxplemfrat  45175  binomcxplemradcnv  45176  binomcxplemcvg  45178  binomcxplemdvsum  45179  binomcxplemnotnn0  45180  mapss2  46036  fmuldfeqlem1  46412  clim1fr1  46431  climrec  46433  climexp  46435  climneg  46440  divcnvg  46457  sumnnodd  46460  supcnvlimsup  46568  icccncfext  46715  cncfioobdlem  46724  fprodsubrecnncnvlem  46735  fprodaddrecnncnvlem  46737  dvsinax  46741  fperdvper  46747  dvcosax  46754  ioodvbdlimc1lem2  46760  ioodvbdlimc2lem  46762  dvnmul  46771  dvnprodlem1  46774  dvnprodlem2  46775  dvnprodlem3  46776  itgsinexp  46783  itgcoscmulx  46797  itgsincmulx  46802  itgsubsticclem  46803  itgsubsticc  46804  itgiccshift  46808  wallispilem5  46897  wallispi  46898  wallispi2lem1  46899  wallispi2lem2  46900  wallispi2  46901  stirlinglem1  46902  stirlinglem2  46903  stirlinglem3  46904  stirlinglem4  46905  stirlinglem5  46906  stirlinglem7  46908  stirlinglem8  46909  stirlinglem10  46911  stirlinglem11  46912  stirlinglem12  46913  stirlinglem13  46914  stirlinglem14  46915  stirlinglem15  46916  dirkerval2  46922  dirkercncflem2  46932  fourierdlem7  46942  fourierdlem13  46948  fourierdlem14  46949  fourierdlem16  46951  fourierdlem18  46953  fourierdlem19  46954  fourierdlem21  46956  fourierdlem22  46957  fourierdlem26  46961  fourierdlem37  46972  fourierdlem39  46974  fourierdlem41  46976  fourierdlem50  46984  fourierdlem51  46985  fourierdlem53  46987  fourierdlem62  46996  fourierdlem63  46997  fourierdlem65  46999  fourierdlem73  47007  fourierdlem74  47008  fourierdlem75  47009  fourierdlem76  47010  fourierdlem79  47013  fourierdlem81  47015  fourierdlem82  47016  fourierdlem83  47017  fourierdlem84  47018  fourierdlem88  47022  fourierdlem89  47023  fourierdlem90  47024  fourierdlem91  47025  fourierdlem92  47026  fourierdlem93  47027  fourierdlem97  47031  fourierdlem101  47035  fourierdlem103  47037  fourierdlem104  47038  fourierdlem111  47045  fourierdlem112  47046  fouriersw  47059  elaa2lem  47061  etransclem13  47075  etransclem17  47079  etransclem18  47080  etransclem21  47083  etransclem31  47093  etransclem32  47094  etransclem33  47095  etransclem35  47097  etransclem46  47108  etransclem48  47110  rrxtopnfi  47115  salgenval  47149  sge0val  47194  sge0z  47203  sge0snmpt  47211  sge0xp  47257  nnfoctbdjlem  47283  omeiunltfirp  47347  caratheodorylem1  47354  0ome  47357  ovnval2  47373  hoicvr  47376  ovncvrrp  47392  ovn0lem  47393  ovnsubaddlem1  47398  hsphoif  47404  hsphoival  47407  hoidmv1le  47422  hoidmvlelem3  47425  ovnhoilem2  47430  ovncvr2  47439  hoidifhspval2  47443  hoidifhspval3  47447  hspmbllem2  47455  smfid  47580  fsetsnf1  47940  fsetsnfo  47941  cfsetsnfsetfv  47945  cfsetsnfsetfo  47948  fvmptrab  48180  fundcmpsurinjlem3  48300  sprval  48379  prproropreud  48409  upgrimwlklem3  48815  grtri  48856  stgrfv  48869  isubgr3stgrlem5  48886  rngcvalALTV  49180  rngcidALTV  49189  rhmsubcALTVlem3  49198  ringcvalALTV  49204  funcringcsetcALTV2lem1  49205  ringcidALTV  49223  funcringcsetclem1ALTV  49228  scmsuppss  49301  ply1mulgsum  49320  lindslinindsimp1  49387  lindsrng01  49398  islindeps2  49413  fdivmptfv  49475  refdivmptfv  49476  1arympt1fv  49569  itcoval0  49592  itcoval1  49593  itcoval2  49594  itcoval3  49595  itcovalsuc  49597  ackvalsuc1mpt  49608  ackvalsuc1  49609  ackval1  49611  ackval2  49612  ackval3  49613  ackval0val  49616  swapf1a  50195  swapf2a  50197  swapf1  50198  swapf2  50200  tposcurf2val  50227  fuco23  50267  prcof1  50314  prcof21a  50317  mndtcid  50515  veronesev1lem  50806  veronesev2lem  50807  veronesev3lem  50808  veronesev4lem  50809  veronesev5lem  50810  veronesev6lem  50811  amgmwlem  50820