Theorem fvmptd 7005

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2105   ↦ cmpt 5231  ‘cfv 6543

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-iota 6495  df-fun 6545  df-fv 6551

This theorem is referenced by:  fvmptd2  7006  fvmptdv2  7016  fsplitfpar  8109  mpocurryvald  8261  fsetfocdm  8861  ttukeylem3  10512  ccatval1  14534  ccatval2  14535  repswsymb  14731  relexp1g  14980  rtrclreclem1  15011  rtrclreclem4  15015  dfrtrcl2  15016  prmodvdslcmf  16987  prmgap  16999  prmgaplcm  17000  prmgapprmo  17002  prdsvscafval  17433  mrcval  17561  cidval  17628  subcid  17804  idfu2nd  17834  resf2nd  17852  fuccoval  17926  fucid  17934  homaval  17991  idaval  18018  setcid  18046  catcid  18067  estrcid  18095  funcestrcsetclem1  18102  funcsetcestrclem1  18116  prf1  18162  prf2  18164  curf1  18188  curf11  18189  curf2val  18193  hof2  18220  yonedalem4a  18238  vrmdval  18780  smndex1gbas  18825  smndex1gid  18826  smndex1n0mnd  18835  mulgnngsum  19002  pj1val  19611  dpjval  19974  c0mgm  20357  c0mhm  20358  c0snmgmhm  20360  c0snmhm  20361  zrrnghm  20432  zrinitorngc  20534  zrtermorngc  20535  zrtermoringc  20567  sraval  21023  rngqiprngimfv  21146  frlmphl  21646  opsrval  21912  selvfval  21988  selvval  21989  mhpval  21992  mhpsclcl  21999  mhpmulcl  22001  psdfval  22010  psdval  22011  psdcoef  22012  cply1mul  22138  cply1coe0  22143  cply1coe0bi  22144  gsummoncoe1  22148  evls1sca  22162  mvmulfv  22366  mavmulfv  22368  mdetuni0  22443  mat2pmatval  22546  m2cpm  22563  cpm2mval  22572  m2cpminvid2lem  22576  decpmatid  22592  decpmatmullem  22593  pmatcollpw2lem  22599  monmatcollpw  22601  pm2mpfval  22618  mp2pm2mplem4  22631  pm2mpmhmlem2  22641  chpmatval  22653  fcfval  23857  cnextfval  23886  utopsnneiplem  24072  rrxmvallem  25252  rrxmval  25253  itgpowd  25905  taylpval  26218  lgamgulmlem2  26875  lgamcvglem  26885  logexprlim  27071  dchr1  27103  ishlg  28286  mirval  28339  mirfv  28340  ishpg  28443  lmif  28469  islmib  28471  lmodvslmhm  32638  psgnfzto1stlem  32695  tocycfv  32704  sgnsval  32756  evls1fldgencl  33199  minplyval  33221  madjusmdetlem2  33272  zarcls0  33312  zarcls1  33313  zarclsiin  33315  zarclsint  33316  zarclssn  33317  qqhvval  33427  indval  33475  indfval  33478  esummulc1  33543  esumcvg  33548  ofcval  33561  sigagenval  33602  measinb  33683  omsfval  33757  omssubadd  33763  sitgfval  33804  eulerpartlemsv1  33819  eulerpartlems  33823  fibp1  33864  totprobd  33889  probmeasb  33893  dstrvprob  33934  dstfrvinc  33939  dstfrvclim1  33940  ballotlemfval  33952  ballotlemsv  33972  gsumnunsn  34016  signsply0  34026  signstfval  34039  fdvneggt  34076  fdvnegge  34078  itgexpif  34082  breprexplema  34106  vtsval  34113  logdivsqrle  34126  hgt750lemg  34130  afsval  34147  lpadval  34152  cvmliftlem9  34748  goel  34802  satf0suc  34831  sat1el2xp  34834  fmlafv  34835  fmla  34836  fmlasuc0  34839  ex-sategoelel  34876  ex-sategoelelomsuc  34881  mvrsval  34960  mrsubfval  34963  mrsubval  34964  msubfval  34979  msubval  34980  msrval  34993  fwddifval  35604  fwddifnval  35605  knoppcnlem1  35833  knoppcnlem4  35836  knoppcnlem6  35838  knoppcnlem7  35839  bj-imdirval2  36528  bj-iminvval2  36539  bj-fvmptunsn2  36603  bj-endval  36660  poimirlem1  36953  poimirlem2  36954  poimirlem5  36957  poimirlem6  36958  poimirlem7  36959  poimirlem10  36962  poimirlem11  36963  poimirlem12  36964  poimirlem19  36971  poimirlem22  36974  mblfinlem2  36990  areacirc  37045  tendopl2  40112  tendoi2  40130  erngplus2  40139  erngplus2-rN  40147  hlhilset  41269  lcmineqlem12  41372  aks4d1p9  41420  sticksstones2  41430  sticksstones3  41431  sticksstones6  41434  sticksstones7  41435  sticksstones8  41436  sticksstones10  41438  sticksstones12a  41440  sticksstones12  41441  sticksstones17  41446  sticksstones18  41447  sticksstones19  41448  metakunt3  41454  metakunt4  41455  metakunt5  41456  metakunt6  41457  metakunt7  41458  metakunt8  41459  metakunt10  41461  metakunt11  41462  metakunt12  41463  metakunt20  41471  metakunt21  41472  metakunt22  41473  metakunt26  41477  metakunt27  41478  metakunt28  41479  metakunt29  41480  metakunt30  41481  metakunt32  41483  fvmptd4  41520  rfovfvd  43216  rfovfvfvd  43217  rfovcnvf1od  43218  rfovcnvfvd  43221  fsovfvd  43224  fsovfvfvd  43225  fsovcnvlem  43227  dssmapfv2d  43232  dssmapfv3d  43233  dssmapnvod  43234  clsk3nimkb  43254  dvgrat  43534  radcnvrat  43536  hashnzfzclim  43544  binomcxplemnn0  43571  binomcxplemrat  43572  binomcxplemfrat  43573  binomcxplemradcnv  43574  binomcxplemcvg  43576  binomcxplemdvsum  43577  binomcxplemnotnn0  43578  mapss2  44363  fmuldfeqlem1  44757  clim1fr1  44776  climrec  44778  climexp  44780  climneg  44785  divcnvg  44802  sumnnodd  44805  supcnvlimsup  44915  icccncfext  45062  cncfioobdlem  45071  fprodsubrecnncnvlem  45082  fprodaddrecnncnvlem  45084  dvsinax  45088  fperdvper  45094  dvcosax  45101  ioodvbdlimc1lem2  45107  ioodvbdlimc2lem  45109  dvnmul  45118  dvnprodlem1  45121  dvnprodlem2  45122  dvnprodlem3  45123  itgsinexp  45130  itgcoscmulx  45144  itgsincmulx  45149  itgsubsticclem  45150  itgsubsticc  45151  itgiccshift  45155  wallispilem5  45244  wallispi  45245  wallispi2lem1  45246  wallispi2lem2  45247  wallispi2  45248  stirlinglem1  45249  stirlinglem2  45250  stirlinglem3  45251  stirlinglem4  45252  stirlinglem5  45253  stirlinglem7  45255  stirlinglem8  45256  stirlinglem10  45258  stirlinglem11  45259  stirlinglem12  45260  stirlinglem13  45261  stirlinglem14  45262  stirlinglem15  45263  dirkerval2  45269  dirkercncflem2  45279  fourierdlem7  45289  fourierdlem13  45295  fourierdlem14  45296  fourierdlem16  45298  fourierdlem18  45300  fourierdlem19  45301  fourierdlem21  45303  fourierdlem22  45304  fourierdlem26  45308  fourierdlem37  45319  fourierdlem39  45321  fourierdlem41  45323  fourierdlem48  45329  fourierdlem49  45330  fourierdlem50  45331  fourierdlem51  45332  fourierdlem53  45334  fourierdlem62  45343  fourierdlem63  45344  fourierdlem65  45346  fourierdlem73  45354  fourierdlem74  45355  fourierdlem75  45356  fourierdlem76  45357  fourierdlem79  45360  fourierdlem81  45362  fourierdlem82  45363  fourierdlem83  45364  fourierdlem84  45365  fourierdlem88  45369  fourierdlem89  45370  fourierdlem90  45371  fourierdlem91  45372  fourierdlem92  45373  fourierdlem93  45374  fourierdlem97  45378  fourierdlem101  45382  fourierdlem103  45384  fourierdlem104  45385  fourierdlem111  45392  fourierdlem112  45393  fouriersw  45406  elaa2lem  45408  etransclem13  45422  etransclem17  45426  etransclem18  45427  etransclem21  45430  etransclem31  45440  etransclem32  45441  etransclem33  45442  etransclem35  45444  etransclem46  45455  etransclem48  45457  rrxtopnfi  45462  salgenval  45496  sge0val  45541  sge0z  45550  sge0snmpt  45558  sge0xp  45604  nnfoctbdjlem  45630  omeiunltfirp  45694  caratheodorylem1  45701  0ome  45704  ovnval2  45720  hoicvr  45723  ovncvrrp  45739  ovn0lem  45740  ovnsubaddlem1  45745  hsphoif  45751  hsphoival  45754  hoidmv1le  45769  hoidmvlelem3  45772  ovnhoilem2  45777  ovncvr2  45786  hoidifhspval2  45790  hoidifhspval3  45794  hspmbllem2  45802  smfid  45927  fsetsnf1  46221  fsetsnfo  46222  cfsetsnfsetfv  46226  cfsetsnfsetfo  46229  fvmptrab  46459  fundcmpsurinjlem3  46527  sprval  46606  prproropreud  46636  isomuspgrlem2a  46955  rngcvalALTV  47102  rngcidALTV  47111  rhmsubcALTVlem3  47120  ringcvalALTV  47126  funcringcsetcALTV2lem1  47127  ringcidALTV  47145  funcringcsetclem1ALTV  47150  scmsuppss  47211  ply1mulgsum  47233  lindslinindsimp1  47300  lindsrng01  47311  islindeps2  47326  fdivmptfv  47393  refdivmptfv  47394  1arympt1fv  47487  itcoval0  47510  itcoval1  47511  itcoval2  47512  itcoval3  47513  itcovalsuc  47515  ackvalsuc1mpt  47526  ackvalsuc1  47527  ackval1  47529  ackval2  47530  ackval3  47531  ackval0val  47534  mndtcid  47877  amgmwlem  48011