Theorem fvmptd 7003

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

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107   ↦ cmpt 5231  ‘cfv 6541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  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 6493  df-fun 6543  df-fv 6549

This theorem is referenced by:  fvmptd2  7004  fvmptdv2  7014  fsplitfpar  8101  mpocurryvald  8252  fsetfocdm  8852  ttukeylem3  10503  ccatval1  14524  ccatval2  14525  repswsymb  14721  relexp1g  14970  rtrclreclem1  15001  rtrclreclem4  15005  dfrtrcl2  15006  prmodvdslcmf  16977  prmgap  16989  prmgaplcm  16990  prmgapprmo  16992  prdsvscafval  17423  mrcval  17551  cidval  17618  subcid  17794  idfu2nd  17824  resf2nd  17842  fuccoval  17913  fucid  17921  homaval  17978  idaval  18005  setcid  18033  catcid  18054  estrcid  18082  funcestrcsetclem1  18089  funcsetcestrclem1  18103  prf1  18149  prf2  18151  curf1  18175  curf11  18176  curf2val  18180  hof2  18207  yonedalem4a  18225  vrmdval  18735  smndex1gbas  18780  smndex1gid  18781  smndex1n0mnd  18790  mulgnngsum  18954  pj1val  19558  dpjval  19921  sraval  20782  frlmphl  21328  opsrval  21593  selvfval  21672  selvval  21673  mhpval  21675  mhpsclcl  21682  mhpmulcl  21684  cply1mul  21810  cply1coe0  21815  cply1coe0bi  21816  gsummoncoe1  21820  evls1sca  21834  mvmulfv  22038  mavmulfv  22040  mdetuni0  22115  mat2pmatval  22218  m2cpm  22235  cpm2mval  22244  m2cpminvid2lem  22248  decpmatid  22264  decpmatmullem  22265  pmatcollpw2lem  22271  monmatcollpw  22273  pm2mpfval  22290  mp2pm2mplem4  22303  pm2mpmhmlem2  22313  chpmatval  22325  fcfval  23529  cnextfval  23558  utopsnneiplem  23744  rrxmvallem  24913  rrxmval  24914  itgpowd  25559  taylpval  25871  lgamgulmlem2  26524  lgamcvglem  26534  logexprlim  26718  dchr1  26750  ishlg  27843  mirval  27896  mirfv  27897  ishpg  28000  lmif  28026  islmib  28028  lmodvslmhm  32190  psgnfzto1stlem  32247  tocycfv  32256  sgnsval  32308  minplyval  32755  madjusmdetlem2  32797  zarcls0  32837  zarcls1  32838  zarclsiin  32840  zarclsint  32841  zarclssn  32842  qqhvval  32952  indval  33000  indfval  33003  esummulc1  33068  esumcvg  33073  ofcval  33086  sigagenval  33127  measinb  33208  omsfval  33282  omssubadd  33288  sitgfval  33329  eulerpartlemsv1  33344  eulerpartlems  33348  fibp1  33389  totprobd  33414  probmeasb  33418  dstrvprob  33459  dstfrvinc  33464  dstfrvclim1  33465  ballotlemfval  33477  ballotlemsv  33497  gsumnunsn  33541  signsply0  33551  signstfval  33564  fdvneggt  33601  fdvnegge  33603  itgexpif  33607  breprexplema  33631  vtsval  33638  logdivsqrle  33651  hgt750lemg  33655  afsval  33672  lpadval  33677  cvmliftlem9  34273  goel  34327  satf0suc  34356  sat1el2xp  34359  fmlafv  34360  fmla  34361  fmlasuc0  34364  ex-sategoelel  34401  ex-sategoelelomsuc  34406  mvrsval  34485  mrsubfval  34488  mrsubval  34489  msubfval  34504  msubval  34505  msrval  34518  fwddifval  35123  fwddifnval  35124  knoppcnlem1  35358  knoppcnlem4  35361  knoppcnlem6  35363  knoppcnlem7  35364  bj-imdirval2  36053  bj-iminvval2  36064  bj-fvmptunsn2  36128  bj-endval  36185  poimirlem1  36478  poimirlem2  36479  poimirlem5  36482  poimirlem6  36483  poimirlem7  36484  poimirlem10  36487  poimirlem11  36488  poimirlem12  36489  poimirlem19  36496  poimirlem22  36499  mblfinlem2  36515  areacirc  36570  tendopl2  39637  tendoi2  39655  erngplus2  39664  erngplus2-rN  39672  hlhilset  40794  lcmineqlem12  40894  aks4d1p9  40942  sticksstones2  40952  sticksstones3  40953  sticksstones6  40956  sticksstones7  40957  sticksstones8  40958  sticksstones10  40960  sticksstones12a  40962  sticksstones12  40963  sticksstones17  40968  sticksstones18  40969  sticksstones19  40970  metakunt3  40976  metakunt4  40977  metakunt5  40978  metakunt6  40979  metakunt7  40980  metakunt8  40981  metakunt10  40983  metakunt11  40984  metakunt12  40985  metakunt20  40993  metakunt21  40994  metakunt22  40995  metakunt26  40999  metakunt27  41000  metakunt28  41001  metakunt29  41002  metakunt30  41003  metakunt32  41005  fvmptd4  41051  rfovfvd  42739  rfovfvfvd  42740  rfovcnvf1od  42741  rfovcnvfvd  42744  fsovfvd  42747  fsovfvfvd  42748  fsovcnvlem  42750  dssmapfv2d  42755  dssmapfv3d  42756  dssmapnvod  42757  clsk3nimkb  42777  dvgrat  43057  radcnvrat  43059  hashnzfzclim  43067  binomcxplemnn0  43094  binomcxplemrat  43095  binomcxplemfrat  43096  binomcxplemradcnv  43097  binomcxplemcvg  43099  binomcxplemdvsum  43100  binomcxplemnotnn0  43101  mapss2  43890  fmuldfeqlem1  44285  clim1fr1  44304  climrec  44306  climexp  44308  climneg  44313  divcnvg  44330  sumnnodd  44333  supcnvlimsup  44443  icccncfext  44590  cncfioobdlem  44599  fprodsubrecnncnvlem  44610  fprodaddrecnncnvlem  44612  dvsinax  44616  fperdvper  44622  dvcosax  44629  ioodvbdlimc1lem2  44635  ioodvbdlimc2lem  44637  dvnmul  44646  dvnprodlem1  44649  dvnprodlem2  44650  dvnprodlem3  44651  itgsinexp  44658  itgcoscmulx  44672  itgsincmulx  44677  itgsubsticclem  44678  itgsubsticc  44679  itgiccshift  44683  wallispilem5  44772  wallispi  44773  wallispi2lem1  44774  wallispi2lem2  44775  wallispi2  44776  stirlinglem1  44777  stirlinglem2  44778  stirlinglem3  44779  stirlinglem4  44780  stirlinglem5  44781  stirlinglem7  44783  stirlinglem8  44784  stirlinglem10  44786  stirlinglem11  44787  stirlinglem12  44788  stirlinglem13  44789  stirlinglem14  44790  stirlinglem15  44791  dirkerval2  44797  dirkercncflem2  44807  fourierdlem7  44817  fourierdlem13  44823  fourierdlem14  44824  fourierdlem16  44826  fourierdlem18  44828  fourierdlem19  44829  fourierdlem21  44831  fourierdlem22  44832  fourierdlem26  44836  fourierdlem37  44847  fourierdlem39  44849  fourierdlem41  44851  fourierdlem48  44857  fourierdlem49  44858  fourierdlem50  44859  fourierdlem51  44860  fourierdlem53  44862  fourierdlem62  44871  fourierdlem63  44872  fourierdlem65  44874  fourierdlem73  44882  fourierdlem74  44883  fourierdlem75  44884  fourierdlem76  44885  fourierdlem79  44888  fourierdlem81  44890  fourierdlem82  44891  fourierdlem83  44892  fourierdlem84  44893  fourierdlem88  44897  fourierdlem89  44898  fourierdlem90  44899  fourierdlem91  44900  fourierdlem92  44901  fourierdlem93  44902  fourierdlem97  44906  fourierdlem101  44910  fourierdlem103  44912  fourierdlem104  44913  fourierdlem111  44920  fourierdlem112  44921  fouriersw  44934  elaa2lem  44936  etransclem13  44950  etransclem17  44954  etransclem18  44955  etransclem21  44958  etransclem31  44968  etransclem32  44969  etransclem33  44970  etransclem35  44972  etransclem46  44983  etransclem48  44985  rrxtopnfi  44990  salgenval  45024  sge0val  45069  sge0z  45078  sge0snmpt  45086  sge0xp  45132  nnfoctbdjlem  45158  omeiunltfirp  45222  caratheodorylem1  45229  0ome  45232  ovnval2  45248  hoicvr  45251  ovncvrrp  45267  ovn0lem  45268  ovnsubaddlem1  45273  hsphoif  45279  hsphoival  45282  hoidmv1le  45297  hoidmvlelem3  45300  ovnhoilem2  45305  ovncvr2  45314  hoidifhspval2  45318  hoidifhspval3  45322  hspmbllem2  45330  smfid  45455  fsetsnf1  45749  fsetsnfo  45750  cfsetsnfsetfv  45754  cfsetsnfsetfo  45757  fvmptrab  45987  fundcmpsurinjlem3  46055  sprval  46134  prproropreud  46164  isomuspgrlem2a  46483  c0mgm  46694  c0mhm  46695  c0snmgmhm  46699  c0snmhm  46700  zrrnghm  46702  rngqiprngimfv  46764  rngcvalALTV  46813  rngcidALTV  46843  zrinitorngc  46852  zrtermorngc  46853  ringcvalALTV  46859  funcringcsetcALTV2lem1  46888  ringcidALTV  46906  funcringcsetclem1ALTV  46911  zrtermoringc  46922  rhmsubcALTVlem3  46958  scmsuppss  47002  ply1mulgsum  47025  lindslinindsimp1  47092  lindsrng01  47103  islindeps2  47118  fdivmptfv  47185  refdivmptfv  47186  1arympt1fv  47279  itcoval0  47302  itcoval1  47303  itcoval2  47304  itcoval3  47305  itcovalsuc  47307  ackvalsuc1mpt  47318  ackvalsuc1  47319  ackval1  47321  ackval2  47322  ackval3  47323  ackval0val  47326  mndtcid  47669  amgmwlem  47803