Theorem fvmptd 6948

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113   ↦ cmpt 5179  ‘cfv 6492

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-iota 6448  df-fun 6494  df-fv 6500

This theorem is referenced by:  fvmptd2  6949  fvmptdv2  6959  fvmptd4  6965  mptcnfimad  7930  fsplitfpar  8060  mpocurryvald  8212  ttukeylem3  10421  tpf1ofv0  14419  tpf1ofv1  14420  tpf1ofv2  14421  ccatval1  14500  ccatval2  14501  repswsymb  14697  relexp1g  14949  rtrclreclem1  14980  rtrclreclem4  14984  dfrtrcl2  14985  prmodvdslcmf  16975  prmgap  16987  prmgaplcm  16988  prmgapprmo  16990  prdsvscafval  17400  mrcval  17533  cidval  17600  subcid  17771  idfu2nd  17801  resf2nd  17819  fuccoval  17890  fucid  17898  homaval  17955  idaval  17982  setcid  18010  catcid  18031  estrcid  18057  funcestrcsetclem1  18063  funcsetcestrclem1  18077  prf1  18123  prf2  18125  curf1  18148  curf11  18149  curf2val  18153  hof2  18180  yonedalem4a  18198  vrmdval  18782  smndex1gbas  18827  smndex1gid  18828  smndex1n0mnd  18837  mulgnngsum  19009  pj1val  19624  dpjval  19987  c0mgm  20395  c0mhm  20396  c0snmgmhm  20398  c0snmhm  20399  zrrnghm  20469  zrinitorngc  20575  zrtermorngc  20576  zrtermoringc  20608  sraval  21127  rngqiprngimfv  21253  frlmphl  21736  opsrval  22001  selvfval  22077  mhpval  22082  mhpsclcl  22090  psdfval  22101  cply1mul  22240  cply1coe0  22245  cply1coe0bi  22246  gsummoncoe1  22252  evls1sca  22267  mvmulfv  22488  mavmulfv  22490  mdetuni0  22565  mat2pmatval  22668  m2cpm  22685  cpm2mval  22694  m2cpminvid2lem  22698  decpmatid  22714  decpmatmullem  22715  pmatcollpw2lem  22721  monmatcollpw  22723  pm2mpfval  22740  mp2pm2mplem4  22753  pm2mpmhmlem2  22763  chpmatval  22775  fcfval  23977  cnextfval  24006  utopsnneiplem  24191  rrxmvallem  25360  rrxmval  25361  itgpowd  26013  taylpval  26330  lgamgulmlem2  26996  lgamcvglem  27006  logexprlim  27192  dchr1  27224  ishlg  28674  mirval  28727  mirfv  28728  ishpg  28831  lmif  28857  islmib  28859  indval  32932  indfval  32935  lmodvslmhm  33133  psgnfzto1stlem  33182  tocycfv  33191  sgnsval  33243  mplvrpmrhm  33712  esplyfval0  33722  esplyind  33731  evls1fldgencl  33827  minplyval  33862  rtelextdg2lem  33883  2sqr3minply  33937  cos9thpiminply  33945  zarcls0  34025  zarcls1  34026  zarclsiin  34028  zarclsint  34029  zarclssn  34030  qqhvval  34140  esummulc1  34238  esumcvg  34243  ofcval  34256  sigagenval  34297  measinb  34378  omsfval  34451  omssubadd  34457  sitgfval  34498  eulerpartlemsv1  34513  eulerpartlems  34517  fibp1  34558  totprobd  34583  probmeasb  34587  dstrvprob  34629  dstfrvinc  34634  dstfrvclim1  34635  ballotlemfval  34647  ballotlemsv  34667  gsumnunsn  34698  signsply0  34708  signstfval  34721  fdvneggt  34757  fdvnegge  34759  itgexpif  34763  breprexplema  34787  vtsval  34794  logdivsqrle  34807  hgt750lemg  34811  afsval  34828  lpadval  34833  cvmliftlem9  35487  goel  35541  satf0suc  35570  sat1el2xp  35573  fmlafv  35574  fmla  35575  fmlasuc0  35578  ex-sategoelel  35615  ex-sategoelelomsuc  35620  mvrsval  35699  mrsubfval  35702  mrsubval  35703  msubfval  35718  msubval  35719  msrval  35732  fwddifval  36356  fwddifnval  36357  knoppcnlem1  36693  knoppcnlem4  36696  knoppcnlem6  36698  knoppcnlem7  36699  bj-imdirval2  37388  bj-iminvval2  37399  bj-fvmptunsn2  37463  bj-endval  37520  poimirlem1  37822  poimirlem2  37823  poimirlem5  37826  poimirlem6  37827  poimirlem7  37828  poimirlem10  37831  poimirlem11  37832  poimirlem12  37833  poimirlem19  37840  poimirlem22  37843  mblfinlem2  37859  areacirc  37914  tendopl2  41037  tendoi2  41055  erngplus2  41064  erngplus2-rN  41072  hlhilset  42194  rhmzrhval  42225  lcmineqlem12  42294  aks4d1p9  42342  primrootscoprbij  42356  aks6d1c1p3  42364  aks6d1c1p5  42366  aks6d1c1  42370  hashscontpow  42376  aks6d1c3  42377  aks6d1c4  42378  aks6d1c2lem4  42381  aks6d1c2  42384  aks6d1c5lem3  42391  deg1gprod  42394  sticksstones2  42401  sticksstones3  42402  sticksstones6  42405  sticksstones7  42406  sticksstones8  42407  sticksstones10  42409  sticksstones12a  42411  sticksstones12  42412  sticksstones17  42417  sticksstones18  42418  sticksstones19  42419  aks6d1c6lem1  42424  aks6d1c6lem2  42425  aks6d1c6lem3  42426  aks6d1c6lem4  42427  aks6d1c6isolem1  42428  aks6d1c6isolem2  42429  aks6d1c6isolem3  42430  aks6d1c6lem5  42431  aks6d1c7lem1  42434  aks5lem2  42441  aks5lem3a  42443  unitscyglem1  42449  rfovfvd  44243  rfovfvfvd  44244  rfovcnvf1od  44245  rfovcnvfvd  44248  fsovfvd  44251  fsovfvfvd  44252  fsovcnvlem  44254  dssmapfv2d  44259  dssmapfv3d  44260  dssmapnvod  44261  clsk3nimkb  44281  dvgrat  44553  radcnvrat  44555  hashnzfzclim  44563  binomcxplemnn0  44590  binomcxplemrat  44591  binomcxplemfrat  44592  binomcxplemradcnv  44593  binomcxplemcvg  44595  binomcxplemdvsum  44596  binomcxplemnotnn0  44597  mapss2  45449  fmuldfeqlem1  45828  clim1fr1  45847  climrec  45849  climexp  45851  climneg  45856  divcnvg  45873  sumnnodd  45876  supcnvlimsup  45984  icccncfext  46131  cncfioobdlem  46140  fprodsubrecnncnvlem  46151  fprodaddrecnncnvlem  46153  dvsinax  46157  fperdvper  46163  dvcosax  46170  ioodvbdlimc1lem2  46176  ioodvbdlimc2lem  46178  dvnmul  46187  dvnprodlem1  46190  dvnprodlem2  46191  dvnprodlem3  46192  itgsinexp  46199  itgcoscmulx  46213  itgsincmulx  46218  itgsubsticclem  46219  itgsubsticc  46220  itgiccshift  46224  wallispilem5  46313  wallispi  46314  wallispi2lem1  46315  wallispi2lem2  46316  wallispi2  46317  stirlinglem1  46318  stirlinglem2  46319  stirlinglem3  46320  stirlinglem4  46321  stirlinglem5  46322  stirlinglem7  46324  stirlinglem8  46325  stirlinglem10  46327  stirlinglem11  46328  stirlinglem12  46329  stirlinglem13  46330  stirlinglem14  46331  stirlinglem15  46332  dirkerval2  46338  dirkercncflem2  46348  fourierdlem7  46358  fourierdlem13  46364  fourierdlem14  46365  fourierdlem16  46367  fourierdlem18  46369  fourierdlem19  46370  fourierdlem21  46372  fourierdlem22  46373  fourierdlem26  46377  fourierdlem37  46388  fourierdlem39  46390  fourierdlem41  46392  fourierdlem48  46398  fourierdlem49  46399  fourierdlem50  46400  fourierdlem51  46401  fourierdlem53  46403  fourierdlem62  46412  fourierdlem63  46413  fourierdlem65  46415  fourierdlem73  46423  fourierdlem74  46424  fourierdlem75  46425  fourierdlem76  46426  fourierdlem79  46429  fourierdlem81  46431  fourierdlem82  46432  fourierdlem83  46433  fourierdlem84  46434  fourierdlem88  46438  fourierdlem89  46439  fourierdlem90  46440  fourierdlem91  46441  fourierdlem92  46442  fourierdlem93  46443  fourierdlem97  46447  fourierdlem101  46451  fourierdlem103  46453  fourierdlem104  46454  fourierdlem111  46461  fourierdlem112  46462  fouriersw  46475  elaa2lem  46477  etransclem13  46491  etransclem17  46495  etransclem18  46496  etransclem21  46499  etransclem31  46509  etransclem32  46510  etransclem33  46511  etransclem35  46513  etransclem46  46524  etransclem48  46526  rrxtopnfi  46531  salgenval  46565  sge0val  46610  sge0z  46619  sge0snmpt  46627  sge0xp  46673  nnfoctbdjlem  46699  omeiunltfirp  46763  caratheodorylem1  46770  0ome  46773  ovnval2  46789  hoicvr  46792  ovncvrrp  46808  ovn0lem  46809  ovnsubaddlem1  46814  hsphoif  46820  hsphoival  46823  hoidmv1le  46838  hoidmvlelem3  46841  ovnhoilem2  46846  ovncvr2  46855  hoidifhspval2  46859  hoidifhspval3  46863  hspmbllem2  46871  smfid  46996  fsetsnf1  47298  fsetsnfo  47299  cfsetsnfsetfv  47303  cfsetsnfsetfo  47306  fvmptrab  47538  fundcmpsurinjlem3  47646  sprval  47725  prproropreud  47755  upgrimwlklem3  48145  grtri  48186  stgrfv  48199  isubgr3stgrlem5  48216  rngcvalALTV  48511  rngcidALTV  48520  rhmsubcALTVlem3  48529  ringcvalALTV  48535  funcringcsetcALTV2lem1  48536  ringcidALTV  48554  funcringcsetclem1ALTV  48559  scmsuppss  48617  ply1mulgsum  48636  lindslinindsimp1  48703  lindsrng01  48714  islindeps2  48729  fdivmptfv  48791  refdivmptfv  48792  1arympt1fv  48885  itcoval0  48908  itcoval1  48909  itcoval2  48910  itcoval3  48911  itcovalsuc  48913  ackvalsuc1mpt  48924  ackvalsuc1  48925  ackval1  48927  ackval2  48928  ackval3  48929  ackval0val  48932  swapf1a  49514  swapf2a  49516  swapf1  49517  swapf2  49519  tposcurf2val  49546  fuco23  49586  prcof1  49633  prcof21a  49636  mndtcid  49834  amgmwlem  50047