Theorem fvmptd 6957

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114   ↦ cmpt 5181  ‘cfv 6500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-iota 6456  df-fun 6502  df-fv 6508

This theorem is referenced by:  fvmptd2  6958  fvmptdv2  6968  fvmptd4  6974  mptcnfimad  7940  fsplitfpar  8070  mpocurryvald  8222  ttukeylem3  10433  tpf1ofv0  14431  tpf1ofv1  14432  tpf1ofv2  14433  ccatval1  14512  ccatval2  14513  repswsymb  14709  relexp1g  14961  rtrclreclem1  14992  rtrclreclem4  14996  dfrtrcl2  14997  prmodvdslcmf  16987  prmgap  16999  prmgaplcm  17000  prmgapprmo  17002  prdsvscafval  17412  mrcval  17545  cidval  17612  subcid  17783  idfu2nd  17813  resf2nd  17831  fuccoval  17902  fucid  17910  homaval  17967  idaval  17994  setcid  18022  catcid  18043  estrcid  18069  funcestrcsetclem1  18075  funcsetcestrclem1  18089  prf1  18135  prf2  18137  curf1  18160  curf11  18161  curf2val  18165  hof2  18192  yonedalem4a  18210  vrmdval  18794  smndex1gbas  18839  smndex1gid  18840  smndex1n0mnd  18849  mulgnngsum  19021  pj1val  19636  dpjval  19999  c0mgm  20407  c0mhm  20408  c0snmgmhm  20410  c0snmhm  20411  zrrnghm  20481  zrinitorngc  20587  zrtermorngc  20588  zrtermoringc  20620  sraval  21139  rngqiprngimfv  21265  frlmphl  21748  opsrval  22013  selvfval  22089  mhpval  22094  mhpsclcl  22102  psdfval  22113  cply1mul  22252  cply1coe0  22257  cply1coe0bi  22258  gsummoncoe1  22264  evls1sca  22279  mvmulfv  22500  mavmulfv  22502  mdetuni0  22577  mat2pmatval  22680  m2cpm  22697  cpm2mval  22706  m2cpminvid2lem  22710  decpmatid  22726  decpmatmullem  22727  pmatcollpw2lem  22733  monmatcollpw  22735  pm2mpfval  22752  mp2pm2mplem4  22765  pm2mpmhmlem2  22775  chpmatval  22787  fcfval  23989  cnextfval  24018  utopsnneiplem  24203  rrxmvallem  25372  rrxmval  25373  itgpowd  26025  taylpval  26342  lgamgulmlem2  27008  lgamcvglem  27018  logexprlim  27204  dchr1  27236  ishlg  28686  mirval  28739  mirfv  28740  ishpg  28843  lmif  28869  islmib  28871  indval  32942  indfval  32945  lmodvslmhm  33143  psgnfzto1stlem  33193  tocycfv  33202  sgnsval  33254  mplvrpmrhm  33723  esplyfval0  33740  esplyind  33751  evls1fldgencl  33847  minplyval  33882  rtelextdg2lem  33903  2sqr3minply  33957  cos9thpiminply  33965  zarcls0  34045  zarcls1  34046  zarclsiin  34048  zarclsint  34049  zarclssn  34050  qqhvval  34160  esummulc1  34258  esumcvg  34263  ofcval  34276  sigagenval  34317  measinb  34398  omsfval  34471  omssubadd  34477  sitgfval  34518  eulerpartlemsv1  34533  eulerpartlems  34537  fibp1  34578  totprobd  34603  probmeasb  34607  dstrvprob  34649  dstfrvinc  34654  dstfrvclim1  34655  ballotlemfval  34667  ballotlemsv  34687  gsumnunsn  34718  signsply0  34728  signstfval  34741  fdvneggt  34777  fdvnegge  34779  itgexpif  34783  breprexplema  34807  vtsval  34814  logdivsqrle  34827  hgt750lemg  34831  afsval  34848  lpadval  34853  cvmliftlem9  35506  goel  35560  satf0suc  35589  sat1el2xp  35592  fmlafv  35593  fmla  35594  fmlasuc0  35597  ex-sategoelel  35634  ex-sategoelelomsuc  35639  mvrsval  35718  mrsubfval  35721  mrsubval  35722  msubfval  35737  msubval  35738  msrval  35751  fwddifval  36375  fwddifnval  36376  knoppcnlem1  36712  knoppcnlem4  36715  knoppcnlem6  36717  knoppcnlem7  36718  bj-imdirval2  37435  bj-iminvval2  37446  bj-fvmptunsn2  37510  bj-endval  37567  poimirlem1  37869  poimirlem2  37870  poimirlem5  37873  poimirlem6  37874  poimirlem7  37875  poimirlem10  37878  poimirlem11  37879  poimirlem12  37880  poimirlem19  37887  poimirlem22  37890  mblfinlem2  37906  areacirc  37961  tendopl2  41150  tendoi2  41168  erngplus2  41177  erngplus2-rN  41185  hlhilset  42307  rhmzrhval  42338  lcmineqlem12  42407  aks4d1p9  42455  primrootscoprbij  42469  aks6d1c1p3  42477  aks6d1c1p5  42479  aks6d1c1  42483  hashscontpow  42489  aks6d1c3  42490  aks6d1c4  42491  aks6d1c2lem4  42494  aks6d1c2  42497  aks6d1c5lem3  42504  deg1gprod  42507  sticksstones2  42514  sticksstones3  42515  sticksstones6  42518  sticksstones7  42519  sticksstones8  42520  sticksstones10  42522  sticksstones12a  42524  sticksstones12  42525  sticksstones17  42530  sticksstones18  42531  sticksstones19  42532  aks6d1c6lem1  42537  aks6d1c6lem2  42538  aks6d1c6lem3  42539  aks6d1c6lem4  42540  aks6d1c6isolem1  42541  aks6d1c6isolem2  42542  aks6d1c6isolem3  42543  aks6d1c6lem5  42544  aks6d1c7lem1  42547  aks5lem2  42554  aks5lem3a  42556  unitscyglem1  42562  rfovfvd  44355  rfovfvfvd  44356  rfovcnvf1od  44357  rfovcnvfvd  44360  fsovfvd  44363  fsovfvfvd  44364  fsovcnvlem  44366  dssmapfv2d  44371  dssmapfv3d  44372  dssmapnvod  44373  clsk3nimkb  44393  dvgrat  44665  radcnvrat  44667  hashnzfzclim  44675  binomcxplemnn0  44702  binomcxplemrat  44703  binomcxplemfrat  44704  binomcxplemradcnv  44705  binomcxplemcvg  44707  binomcxplemdvsum  44708  binomcxplemnotnn0  44709  mapss2  45560  fmuldfeqlem1  45939  clim1fr1  45958  climrec  45960  climexp  45962  climneg  45967  divcnvg  45984  sumnnodd  45987  supcnvlimsup  46095  icccncfext  46242  cncfioobdlem  46251  fprodsubrecnncnvlem  46262  fprodaddrecnncnvlem  46264  dvsinax  46268  fperdvper  46274  dvcosax  46281  ioodvbdlimc1lem2  46287  ioodvbdlimc2lem  46289  dvnmul  46298  dvnprodlem1  46301  dvnprodlem2  46302  dvnprodlem3  46303  itgsinexp  46310  itgcoscmulx  46324  itgsincmulx  46329  itgsubsticclem  46330  itgsubsticc  46331  itgiccshift  46335  wallispilem5  46424  wallispi  46425  wallispi2lem1  46426  wallispi2lem2  46427  wallispi2  46428  stirlinglem1  46429  stirlinglem2  46430  stirlinglem3  46431  stirlinglem4  46432  stirlinglem5  46433  stirlinglem7  46435  stirlinglem8  46436  stirlinglem10  46438  stirlinglem11  46439  stirlinglem12  46440  stirlinglem13  46441  stirlinglem14  46442  stirlinglem15  46443  dirkerval2  46449  dirkercncflem2  46459  fourierdlem7  46469  fourierdlem13  46475  fourierdlem14  46476  fourierdlem16  46478  fourierdlem18  46480  fourierdlem19  46481  fourierdlem21  46483  fourierdlem22  46484  fourierdlem26  46488  fourierdlem37  46499  fourierdlem39  46501  fourierdlem41  46503  fourierdlem48  46509  fourierdlem49  46510  fourierdlem50  46511  fourierdlem51  46512  fourierdlem53  46514  fourierdlem62  46523  fourierdlem63  46524  fourierdlem65  46526  fourierdlem73  46534  fourierdlem74  46535  fourierdlem75  46536  fourierdlem76  46537  fourierdlem79  46540  fourierdlem81  46542  fourierdlem82  46543  fourierdlem83  46544  fourierdlem84  46545  fourierdlem88  46549  fourierdlem89  46550  fourierdlem90  46551  fourierdlem91  46552  fourierdlem92  46553  fourierdlem93  46554  fourierdlem97  46558  fourierdlem101  46562  fourierdlem103  46564  fourierdlem104  46565  fourierdlem111  46572  fourierdlem112  46573  fouriersw  46586  elaa2lem  46588  etransclem13  46602  etransclem17  46606  etransclem18  46607  etransclem21  46610  etransclem31  46620  etransclem32  46621  etransclem33  46622  etransclem35  46624  etransclem46  46635  etransclem48  46637  rrxtopnfi  46642  salgenval  46676  sge0val  46721  sge0z  46730  sge0snmpt  46738  sge0xp  46784  nnfoctbdjlem  46810  omeiunltfirp  46874  caratheodorylem1  46881  0ome  46884  ovnval2  46900  hoicvr  46903  ovncvrrp  46919  ovn0lem  46920  ovnsubaddlem1  46925  hsphoif  46931  hsphoival  46934  hoidmv1le  46949  hoidmvlelem3  46952  ovnhoilem2  46957  ovncvr2  46966  hoidifhspval2  46970  hoidifhspval3  46974  hspmbllem2  46982  smfid  47107  fsetsnf1  47409  fsetsnfo  47410  cfsetsnfsetfv  47414  cfsetsnfsetfo  47417  fvmptrab  47649  fundcmpsurinjlem3  47757  sprval  47836  prproropreud  47866  upgrimwlklem3  48256  grtri  48297  stgrfv  48310  isubgr3stgrlem5  48327  rngcvalALTV  48622  rngcidALTV  48631  rhmsubcALTVlem3  48640  ringcvalALTV  48646  funcringcsetcALTV2lem1  48647  ringcidALTV  48665  funcringcsetclem1ALTV  48670  scmsuppss  48728  ply1mulgsum  48747  lindslinindsimp1  48814  lindsrng01  48825  islindeps2  48840  fdivmptfv  48902  refdivmptfv  48903  1arympt1fv  48996  itcoval0  49019  itcoval1  49020  itcoval2  49021  itcoval3  49022  itcovalsuc  49024  ackvalsuc1mpt  49035  ackvalsuc1  49036  ackval1  49038  ackval2  49039  ackval3  49040  ackval0val  49043  swapf1a  49625  swapf2a  49627  swapf1  49628  swapf2  49630  tposcurf2val  49657  fuco23  49697  prcof1  49744  prcof21a  49747  mndtcid  49945  amgmwlem  50158