Theorem fvmptd 7023

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

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

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 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-iota 6514  df-fun 6563  df-fv 6569

This theorem is referenced by:  fvmptd2  7024  fvmptdv2  7034  fvmptd4  7040  mptcnfimad  8011  fsplitfpar  8143  mpocurryvald  8295  ttukeylem3  10551  tpf1ofv0  14535  tpf1ofv1  14536  tpf1ofv2  14537  ccatval1  14615  ccatval2  14616  repswsymb  14812  relexp1g  15065  rtrclreclem1  15096  rtrclreclem4  15100  dfrtrcl2  15101  prmodvdslcmf  17085  prmgap  17097  prmgaplcm  17098  prmgapprmo  17100  prdsvscafval  17525  mrcval  17653  cidval  17720  subcid  17892  idfu2nd  17922  resf2nd  17940  fuccoval  18011  fucid  18019  homaval  18076  idaval  18103  setcid  18131  catcid  18152  estrcid  18178  funcestrcsetclem1  18185  funcsetcestrclem1  18199  prf1  18245  prf2  18247  curf1  18270  curf11  18271  curf2val  18275  hof2  18302  yonedalem4a  18320  vrmdval  18870  smndex1gbas  18915  smndex1gid  18916  smndex1n0mnd  18925  mulgnngsum  19097  pj1val  19713  dpjval  20076  c0mgm  20459  c0mhm  20460  c0snmgmhm  20462  c0snmhm  20463  zrrnghm  20536  zrinitorngc  20642  zrtermorngc  20643  zrtermoringc  20675  sraval  21174  rngqiprngimfv  21308  frlmphl  21801  opsrval  22064  selvfval  22138  mhpval  22143  mhpsclcl  22151  psdfval  22162  cply1mul  22300  cply1coe0  22305  cply1coe0bi  22306  gsummoncoe1  22312  evls1sca  22327  mvmulfv  22550  mavmulfv  22552  mdetuni0  22627  mat2pmatval  22730  m2cpm  22747  cpm2mval  22756  m2cpminvid2lem  22760  decpmatid  22776  decpmatmullem  22777  pmatcollpw2lem  22783  monmatcollpw  22785  pm2mpfval  22802  mp2pm2mplem4  22815  pm2mpmhmlem2  22825  chpmatval  22837  fcfval  24041  cnextfval  24070  utopsnneiplem  24256  rrxmvallem  25438  rrxmval  25439  itgpowd  26091  taylpval  26408  lgamgulmlem2  27073  lgamcvglem  27083  logexprlim  27269  dchr1  27301  ishlg  28610  mirval  28663  mirfv  28664  ishpg  28767  lmif  28793  islmib  28795  indval  32838  indfval  32841  lmodvslmhm  33053  psgnfzto1stlem  33120  tocycfv  33129  sgnsval  33181  evls1fldgencl  33720  minplyval  33748  rtelextdg2lem  33767  2sqr3minply  33791  zarcls0  33867  zarcls1  33868  zarclsiin  33870  zarclsint  33871  zarclssn  33872  qqhvval  33984  esummulc1  34082  esumcvg  34087  ofcval  34100  sigagenval  34141  measinb  34222  omsfval  34296  omssubadd  34302  sitgfval  34343  eulerpartlemsv1  34358  eulerpartlems  34362  fibp1  34403  totprobd  34428  probmeasb  34432  dstrvprob  34474  dstfrvinc  34479  dstfrvclim1  34480  ballotlemfval  34492  ballotlemsv  34512  gsumnunsn  34556  signsply0  34566  signstfval  34579  fdvneggt  34615  fdvnegge  34617  itgexpif  34621  breprexplema  34645  vtsval  34652  logdivsqrle  34665  hgt750lemg  34669  afsval  34686  lpadval  34691  cvmliftlem9  35298  goel  35352  satf0suc  35381  sat1el2xp  35384  fmlafv  35385  fmla  35386  fmlasuc0  35389  ex-sategoelel  35426  ex-sategoelelomsuc  35431  mvrsval  35510  mrsubfval  35513  mrsubval  35514  msubfval  35529  msubval  35530  msrval  35543  fwddifval  36163  fwddifnval  36164  knoppcnlem1  36494  knoppcnlem4  36497  knoppcnlem6  36499  knoppcnlem7  36500  bj-imdirval2  37184  bj-iminvval2  37195  bj-fvmptunsn2  37259  bj-endval  37316  poimirlem1  37628  poimirlem2  37629  poimirlem5  37632  poimirlem6  37633  poimirlem7  37634  poimirlem10  37637  poimirlem11  37638  poimirlem12  37639  poimirlem19  37646  poimirlem22  37649  mblfinlem2  37665  areacirc  37720  tendopl2  40779  tendoi2  40797  erngplus2  40806  erngplus2-rN  40814  hlhilset  41936  rhmzrhval  41971  lcmineqlem12  42041  aks4d1p9  42089  primrootscoprbij  42103  aks6d1c1p3  42111  aks6d1c1p5  42113  aks6d1c1  42117  hashscontpow  42123  aks6d1c3  42124  aks6d1c4  42125  aks6d1c2lem4  42128  aks6d1c2  42131  aks6d1c5lem3  42138  deg1gprod  42141  sticksstones2  42148  sticksstones3  42149  sticksstones6  42152  sticksstones7  42153  sticksstones8  42154  sticksstones10  42156  sticksstones12a  42158  sticksstones12  42159  sticksstones17  42164  sticksstones18  42165  sticksstones19  42166  aks6d1c6lem1  42171  aks6d1c6lem2  42172  aks6d1c6lem3  42173  aks6d1c6lem4  42174  aks6d1c6isolem1  42175  aks6d1c6isolem2  42176  aks6d1c6isolem3  42177  aks6d1c6lem5  42178  aks6d1c7lem1  42181  aks5lem2  42188  aks5lem3a  42190  unitscyglem1  42196  metakunt3  42208  metakunt4  42209  metakunt5  42210  metakunt6  42211  metakunt7  42212  metakunt8  42213  metakunt10  42215  metakunt11  42216  metakunt12  42217  metakunt20  42225  metakunt21  42226  metakunt22  42227  metakunt26  42231  metakunt27  42232  metakunt28  42233  metakunt29  42234  metakunt30  42235  metakunt32  42237  rfovfvd  44015  rfovfvfvd  44016  rfovcnvf1od  44017  rfovcnvfvd  44020  fsovfvd  44023  fsovfvfvd  44024  fsovcnvlem  44026  dssmapfv2d  44031  dssmapfv3d  44032  dssmapnvod  44033  clsk3nimkb  44053  dvgrat  44331  radcnvrat  44333  hashnzfzclim  44341  binomcxplemnn0  44368  binomcxplemrat  44369  binomcxplemfrat  44370  binomcxplemradcnv  44371  binomcxplemcvg  44373  binomcxplemdvsum  44374  binomcxplemnotnn0  44375  mapss2  45210  fmuldfeqlem1  45597  clim1fr1  45616  climrec  45618  climexp  45620  climneg  45625  divcnvg  45642  sumnnodd  45645  supcnvlimsup  45755  icccncfext  45902  cncfioobdlem  45911  fprodsubrecnncnvlem  45922  fprodaddrecnncnvlem  45924  dvsinax  45928  fperdvper  45934  dvcosax  45941  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  dvnmul  45958  dvnprodlem1  45961  dvnprodlem2  45962  dvnprodlem3  45963  itgsinexp  45970  itgcoscmulx  45984  itgsincmulx  45989  itgsubsticclem  45990  itgsubsticc  45991  itgiccshift  45995  wallispilem5  46084  wallispi  46085  wallispi2lem1  46086  wallispi2lem2  46087  wallispi2  46088  stirlinglem1  46089  stirlinglem2  46090  stirlinglem3  46091  stirlinglem4  46092  stirlinglem5  46093  stirlinglem7  46095  stirlinglem8  46096  stirlinglem10  46098  stirlinglem11  46099  stirlinglem12  46100  stirlinglem13  46101  stirlinglem14  46102  stirlinglem15  46103  dirkerval2  46109  dirkercncflem2  46119  fourierdlem7  46129  fourierdlem13  46135  fourierdlem14  46136  fourierdlem16  46138  fourierdlem18  46140  fourierdlem19  46141  fourierdlem21  46143  fourierdlem22  46144  fourierdlem26  46148  fourierdlem37  46159  fourierdlem39  46161  fourierdlem41  46163  fourierdlem48  46169  fourierdlem49  46170  fourierdlem50  46171  fourierdlem51  46172  fourierdlem53  46174  fourierdlem62  46183  fourierdlem63  46184  fourierdlem65  46186  fourierdlem73  46194  fourierdlem74  46195  fourierdlem75  46196  fourierdlem76  46197  fourierdlem79  46200  fourierdlem81  46202  fourierdlem82  46203  fourierdlem83  46204  fourierdlem84  46205  fourierdlem88  46209  fourierdlem89  46210  fourierdlem90  46211  fourierdlem91  46212  fourierdlem92  46213  fourierdlem93  46214  fourierdlem97  46218  fourierdlem101  46222  fourierdlem103  46224  fourierdlem104  46225  fourierdlem111  46232  fourierdlem112  46233  fouriersw  46246  elaa2lem  46248  etransclem13  46262  etransclem17  46266  etransclem18  46267  etransclem21  46270  etransclem31  46280  etransclem32  46281  etransclem33  46282  etransclem35  46284  etransclem46  46295  etransclem48  46297  rrxtopnfi  46302  salgenval  46336  sge0val  46381  sge0z  46390  sge0snmpt  46398  sge0xp  46444  nnfoctbdjlem  46470  omeiunltfirp  46534  caratheodorylem1  46541  0ome  46544  ovnval2  46560  hoicvr  46563  ovncvrrp  46579  ovn0lem  46580  ovnsubaddlem1  46585  hsphoif  46591  hsphoival  46594  hoidmv1le  46609  hoidmvlelem3  46612  ovnhoilem2  46617  ovncvr2  46626  hoidifhspval2  46630  hoidifhspval3  46634  hspmbllem2  46642  smfid  46767  fsetsnf1  47064  fsetsnfo  47065  cfsetsnfsetfv  47069  cfsetsnfsetfo  47072  fvmptrab  47304  fundcmpsurinjlem3  47387  sprval  47466  prproropreud  47496  grtri  47907  stgrfv  47920  isubgr3stgrlem5  47937  rngcvalALTV  48181  rngcidALTV  48190  rhmsubcALTVlem3  48199  ringcvalALTV  48205  funcringcsetcALTV2lem1  48206  ringcidALTV  48224  funcringcsetclem1ALTV  48229  scmsuppss  48287  ply1mulgsum  48307  lindslinindsimp1  48374  lindsrng01  48385  islindeps2  48400  fdivmptfv  48466  refdivmptfv  48467  1arympt1fv  48560  itcoval0  48583  itcoval1  48584  itcoval2  48585  itcoval3  48586  itcovalsuc  48588  ackvalsuc1mpt  48599  ackvalsuc1  48600  ackval1  48602  ackval2  48603  ackval3  48604  ackval0val  48607  swapf1a  48975  swapf2a  48977  swapf1  48978  swapf2  48980  tposcurf2val  49001  fuco23  49036  mndtcid  49186  amgmwlem  49321