Theorem fvmptd 6941

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ↦ cmpt 5176  ‘cfv 6486

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-iota 6442  df-fun 6488  df-fv 6494

This theorem is referenced by:  fvmptd2  6942  fvmptdv2  6952  fvmptd4  6958  mptcnfimad  7928  fsplitfpar  8058  mpocurryvald  8210  ttukeylem3  10424  tpf1ofv0  14421  tpf1ofv1  14422  tpf1ofv2  14423  ccatval1  14502  ccatval2  14503  repswsymb  14698  relexp1g  14951  rtrclreclem1  14982  rtrclreclem4  14986  dfrtrcl2  14987  prmodvdslcmf  16977  prmgap  16989  prmgaplcm  16990  prmgapprmo  16992  prdsvscafval  17402  mrcval  17534  cidval  17601  subcid  17772  idfu2nd  17802  resf2nd  17820  fuccoval  17891  fucid  17899  homaval  17956  idaval  17983  setcid  18011  catcid  18032  estrcid  18058  funcestrcsetclem1  18064  funcsetcestrclem1  18078  prf1  18124  prf2  18126  curf1  18149  curf11  18150  curf2val  18154  hof2  18181  yonedalem4a  18199  vrmdval  18749  smndex1gbas  18794  smndex1gid  18795  smndex1n0mnd  18804  mulgnngsum  18976  pj1val  19592  dpjval  19955  c0mgm  20362  c0mhm  20363  c0snmgmhm  20365  c0snmhm  20366  zrrnghm  20439  zrinitorngc  20545  zrtermorngc  20546  zrtermoringc  20578  sraval  21097  rngqiprngimfv  21223  frlmphl  21706  opsrval  21969  selvfval  22037  mhpval  22042  mhpsclcl  22050  psdfval  22061  cply1mul  22199  cply1coe0  22204  cply1coe0bi  22205  gsummoncoe1  22211  evls1sca  22226  mvmulfv  22447  mavmulfv  22449  mdetuni0  22524  mat2pmatval  22627  m2cpm  22644  cpm2mval  22653  m2cpminvid2lem  22657  decpmatid  22673  decpmatmullem  22674  pmatcollpw2lem  22680  monmatcollpw  22682  pm2mpfval  22699  mp2pm2mplem4  22712  pm2mpmhmlem2  22722  chpmatval  22734  fcfval  23936  cnextfval  23965  utopsnneiplem  24151  rrxmvallem  25320  rrxmval  25321  itgpowd  25973  taylpval  26290  lgamgulmlem2  26956  lgamcvglem  26966  logexprlim  27152  dchr1  27184  ishlg  28565  mirval  28618  mirfv  28619  ishpg  28722  lmif  28748  islmib  28750  indval  32809  indfval  32812  lmodvslmhm  33016  psgnfzto1stlem  33055  tocycfv  33064  sgnsval  33116  evls1fldgencl  33644  minplyval  33674  rtelextdg2lem  33695  2sqr3minply  33749  cos9thpiminply  33757  zarcls0  33837  zarcls1  33838  zarclsiin  33840  zarclsint  33841  zarclssn  33842  qqhvval  33952  esummulc1  34050  esumcvg  34055  ofcval  34068  sigagenval  34109  measinb  34190  omsfval  34264  omssubadd  34270  sitgfval  34311  eulerpartlemsv1  34326  eulerpartlems  34330  fibp1  34371  totprobd  34396  probmeasb  34400  dstrvprob  34442  dstfrvinc  34447  dstfrvclim1  34448  ballotlemfval  34460  ballotlemsv  34480  gsumnunsn  34511  signsply0  34521  signstfval  34534  fdvneggt  34570  fdvnegge  34572  itgexpif  34576  breprexplema  34600  vtsval  34607  logdivsqrle  34620  hgt750lemg  34624  afsval  34641  lpadval  34646  cvmliftlem9  35268  goel  35322  satf0suc  35351  sat1el2xp  35354  fmlafv  35355  fmla  35356  fmlasuc0  35359  ex-sategoelel  35396  ex-sategoelelomsuc  35401  mvrsval  35480  mrsubfval  35483  mrsubval  35484  msubfval  35499  msubval  35500  msrval  35513  fwddifval  36138  fwddifnval  36139  knoppcnlem1  36469  knoppcnlem4  36472  knoppcnlem6  36474  knoppcnlem7  36475  bj-imdirval2  37159  bj-iminvval2  37170  bj-fvmptunsn2  37234  bj-endval  37291  poimirlem1  37603  poimirlem2  37604  poimirlem5  37607  poimirlem6  37608  poimirlem7  37609  poimirlem10  37612  poimirlem11  37613  poimirlem12  37614  poimirlem19  37621  poimirlem22  37624  mblfinlem2  37640  areacirc  37695  tendopl2  40759  tendoi2  40777  erngplus2  40786  erngplus2-rN  40794  hlhilset  41916  rhmzrhval  41947  lcmineqlem12  42016  aks4d1p9  42064  primrootscoprbij  42078  aks6d1c1p3  42086  aks6d1c1p5  42088  aks6d1c1  42092  hashscontpow  42098  aks6d1c3  42099  aks6d1c4  42100  aks6d1c2lem4  42103  aks6d1c2  42106  aks6d1c5lem3  42113  deg1gprod  42116  sticksstones2  42123  sticksstones3  42124  sticksstones6  42127  sticksstones7  42128  sticksstones8  42129  sticksstones10  42131  sticksstones12a  42133  sticksstones12  42134  sticksstones17  42139  sticksstones18  42140  sticksstones19  42141  aks6d1c6lem1  42146  aks6d1c6lem2  42147  aks6d1c6lem3  42148  aks6d1c6lem4  42149  aks6d1c6isolem1  42150  aks6d1c6isolem2  42151  aks6d1c6isolem3  42152  aks6d1c6lem5  42153  aks6d1c7lem1  42156  aks5lem2  42163  aks5lem3a  42165  unitscyglem1  42171  rfovfvd  43978  rfovfvfvd  43979  rfovcnvf1od  43980  rfovcnvfvd  43983  fsovfvd  43986  fsovfvfvd  43987  fsovcnvlem  43989  dssmapfv2d  43994  dssmapfv3d  43995  dssmapnvod  43996  clsk3nimkb  44016  dvgrat  44288  radcnvrat  44290  hashnzfzclim  44298  binomcxplemnn0  44325  binomcxplemrat  44326  binomcxplemfrat  44327  binomcxplemradcnv  44328  binomcxplemcvg  44330  binomcxplemdvsum  44331  binomcxplemnotnn0  44332  mapss2  45186  fmuldfeqlem1  45567  clim1fr1  45586  climrec  45588  climexp  45590  climneg  45595  divcnvg  45612  sumnnodd  45615  supcnvlimsup  45725  icccncfext  45872  cncfioobdlem  45881  fprodsubrecnncnvlem  45892  fprodaddrecnncnvlem  45894  dvsinax  45898  fperdvper  45904  dvcosax  45911  ioodvbdlimc1lem2  45917  ioodvbdlimc2lem  45919  dvnmul  45928  dvnprodlem1  45931  dvnprodlem2  45932  dvnprodlem3  45933  itgsinexp  45940  itgcoscmulx  45954  itgsincmulx  45959  itgsubsticclem  45960  itgsubsticc  45961  itgiccshift  45965  wallispilem5  46054  wallispi  46055  wallispi2lem1  46056  wallispi2lem2  46057  wallispi2  46058  stirlinglem1  46059  stirlinglem2  46060  stirlinglem3  46061  stirlinglem4  46062  stirlinglem5  46063  stirlinglem7  46065  stirlinglem8  46066  stirlinglem10  46068  stirlinglem11  46069  stirlinglem12  46070  stirlinglem13  46071  stirlinglem14  46072  stirlinglem15  46073  dirkerval2  46079  dirkercncflem2  46089  fourierdlem7  46099  fourierdlem13  46105  fourierdlem14  46106  fourierdlem16  46108  fourierdlem18  46110  fourierdlem19  46111  fourierdlem21  46113  fourierdlem22  46114  fourierdlem26  46118  fourierdlem37  46129  fourierdlem39  46131  fourierdlem41  46133  fourierdlem48  46139  fourierdlem49  46140  fourierdlem50  46141  fourierdlem51  46142  fourierdlem53  46144  fourierdlem62  46153  fourierdlem63  46154  fourierdlem65  46156  fourierdlem73  46164  fourierdlem74  46165  fourierdlem75  46166  fourierdlem76  46167  fourierdlem79  46170  fourierdlem81  46172  fourierdlem82  46173  fourierdlem83  46174  fourierdlem84  46175  fourierdlem88  46179  fourierdlem89  46180  fourierdlem90  46181  fourierdlem91  46182  fourierdlem92  46183  fourierdlem93  46184  fourierdlem97  46188  fourierdlem101  46192  fourierdlem103  46194  fourierdlem104  46195  fourierdlem111  46202  fourierdlem112  46203  fouriersw  46216  elaa2lem  46218  etransclem13  46232  etransclem17  46236  etransclem18  46237  etransclem21  46240  etransclem31  46250  etransclem32  46251  etransclem33  46252  etransclem35  46254  etransclem46  46265  etransclem48  46267  rrxtopnfi  46272  salgenval  46306  sge0val  46351  sge0z  46360  sge0snmpt  46368  sge0xp  46414  nnfoctbdjlem  46440  omeiunltfirp  46504  caratheodorylem1  46511  0ome  46514  ovnval2  46530  hoicvr  46533  ovncvrrp  46549  ovn0lem  46550  ovnsubaddlem1  46555  hsphoif  46561  hsphoival  46564  hoidmv1le  46579  hoidmvlelem3  46582  ovnhoilem2  46587  ovncvr2  46596  hoidifhspval2  46600  hoidifhspval3  46604  hspmbllem2  46612  smfid  46737  fsetsnf1  47040  fsetsnfo  47041  cfsetsnfsetfv  47045  cfsetsnfsetfo  47048  fvmptrab  47280  fundcmpsurinjlem3  47388  sprval  47467  prproropreud  47497  upgrimwlklem3  47887  grtri  47928  stgrfv  47941  isubgr3stgrlem5  47958  rngcvalALTV  48253  rngcidALTV  48262  rhmsubcALTVlem3  48271  ringcvalALTV  48277  funcringcsetcALTV2lem1  48278  ringcidALTV  48296  funcringcsetclem1ALTV  48301  scmsuppss  48359  ply1mulgsum  48379  lindslinindsimp1  48446  lindsrng01  48457  islindeps2  48472  fdivmptfv  48534  refdivmptfv  48535  1arympt1fv  48628  itcoval0  48651  itcoval1  48652  itcoval2  48653  itcoval3  48654  itcovalsuc  48656  ackvalsuc1mpt  48667  ackvalsuc1  48668  ackval1  48670  ackval2  48671  ackval3  48672  ackval0val  48675  swapf1a  49258  swapf2a  49260  swapf1  49261  swapf2  49263  tposcurf2val  49290  fuco23  49330  prcof1  49377  prcof21a  49380  mndtcid  49578  amgmwlem  49791