Theorem fvmptd 6949

Description: Deduction version of fvmpt 6941. (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 6948	1 ⊢ (𝜑 → (𝐹‘𝐴) = 𝐶)

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

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 5231  ax-pr 5370

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 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-iota 6448  df-fun 6494  df-fv 6500

This theorem is referenced by:  fvmptd2  6950  fvmptdv2  6960  fvmptd4  6966  mptcnfimad  7932  fsplitfpar  8061  mpocurryvald  8213  ttukeylem3  10424  indval  12153  indfval  12157  tpf1ofv0  14449  tpf1ofv1  14450  tpf1ofv2  14451  ccatval1  14530  ccatval2  14531  repswsymb  14727  relexp1g  14979  rtrclreclem1  15010  rtrclreclem4  15014  dfrtrcl2  15015  prmodvdslcmf  17009  prmgap  17021  prmgaplcm  17022  prmgapprmo  17024  prdsvscafval  17434  mrcval  17567  cidval  17634  subcid  17805  idfu2nd  17835  resf2nd  17853  fuccoval  17924  fucid  17932  homaval  17989  idaval  18016  setcid  18044  catcid  18065  estrcid  18091  funcestrcsetclem1  18097  funcsetcestrclem1  18111  prf1  18157  prf2  18159  curf1  18182  curf11  18183  curf2val  18187  hof2  18214  yonedalem4a  18232  vrmdval  18816  smndex1gbasOLD  18862  smndex1gid  18863  smndex1gidOLD  18864  smndex1n0mnd  18874  mulgnngsum  19046  pj1val  19661  dpjval  20024  c0mgm  20430  c0mhm  20431  c0snmgmhm  20433  c0snmhm  20434  zrrnghm  20504  zrinitorngc  20610  zrtermorngc  20611  zrtermoringc  20643  sraval  21162  rngqiprngimfv  21288  frlmphl  21771  opsrval  22034  selvfval  22110  mhpval  22115  mhpsclcl  22123  psdfval  22134  cply1mul  22271  cply1coe0  22276  cply1coe0bi  22277  gsummoncoe1  22283  evls1sca  22298  mvmulfv  22519  mavmulfv  22521  mdetuni0  22596  mat2pmatval  22699  m2cpm  22716  cpm2mval  22725  m2cpminvid2lem  22729  decpmatid  22745  decpmatmullem  22746  pmatcollpw2lem  22752  monmatcollpw  22754  pm2mpfval  22771  mp2pm2mplem4  22784  pm2mpmhmlem2  22794  chpmatval  22806  fcfval  24008  cnextfval  24037  utopsnneiplem  24222  rrxmvallem  25381  rrxmval  25382  itgpowd  26027  taylpval  26343  lgamgulmlem2  27007  lgamcvglem  27017  logexprlim  27202  dchr1  27234  ishlg  28684  mirval  28737  mirfv  28738  ishpg  28841  lmif  28867  islmib  28869  lmodvslmhm  33126  psgnfzto1stlem  33176  tocycfv  33185  sgnsval  33237  mplvrpmrhm  33706  esplyfval0  33723  esplyind  33734  evls1fldgencl  33830  minplyval  33865  rtelextdg2lem  33886  2sqr3minply  33940  cos9thpiminply  33948  zarcls0  34028  zarcls1  34029  zarclsiin  34031  zarclsint  34032  zarclssn  34033  qqhvval  34143  esummulc1  34241  esumcvg  34246  ofcval  34259  sigagenval  34300  measinb  34381  omsfval  34454  omssubadd  34460  sitgfval  34501  eulerpartlemsv1  34516  eulerpartlems  34520  fibp1  34561  totprobd  34586  probmeasb  34590  dstrvprob  34632  dstfrvinc  34637  dstfrvclim1  34638  ballotlemfval  34650  ballotlemsv  34670  gsumnunsn  34701  signsply0  34711  signstfval  34724  fdvneggt  34760  fdvnegge  34762  itgexpif  34766  breprexplema  34790  vtsval  34797  logdivsqrle  34810  hgt750lemg  34814  afsval  34831  lpadval  34836  cvmliftlem9  35491  goel  35545  satf0suc  35574  sat1el2xp  35577  fmlafv  35578  fmla  35579  fmlasuc0  35582  ex-sategoelel  35619  ex-sategoelelomsuc  35624  mvrsval  35703  mrsubfval  35706  mrsubval  35707  msubfval  35722  msubval  35723  msrval  35736  fwddifval  36360  fwddifnval  36361  knoppcnlem1  36769  knoppcnlem4  36772  knoppcnlem6  36774  knoppcnlem7  36775  bj-imdirval2  37513  bj-iminvval2  37524  bj-fvmptunsn2  37588  bj-endval  37645  poimirlem1  37956  poimirlem2  37957  poimirlem5  37960  poimirlem6  37961  poimirlem7  37962  poimirlem10  37965  poimirlem11  37966  poimirlem12  37967  poimirlem19  37974  poimirlem22  37977  mblfinlem2  37993  areacirc  38048  tendopl2  41237  tendoi2  41255  erngplus2  41264  erngplus2-rN  41272  hlhilset  42394  rhmzrhval  42425  lcmineqlem12  42493  aks4d1p9  42541  primrootscoprbij  42555  aks6d1c1p3  42563  aks6d1c1p5  42565  aks6d1c1  42569  hashscontpow  42575  aks6d1c3  42576  aks6d1c4  42577  aks6d1c2lem4  42580  aks6d1c2  42583  aks6d1c5lem3  42590  deg1gprod  42593  sticksstones2  42600  sticksstones3  42601  sticksstones6  42604  sticksstones7  42605  sticksstones8  42606  sticksstones10  42608  sticksstones12a  42610  sticksstones12  42611  sticksstones17  42616  sticksstones18  42617  sticksstones19  42618  aks6d1c6lem1  42623  aks6d1c6lem2  42624  aks6d1c6lem3  42625  aks6d1c6lem4  42626  aks6d1c6isolem1  42627  aks6d1c6isolem2  42628  aks6d1c6isolem3  42629  aks6d1c6lem5  42630  aks6d1c7lem1  42633  aks5lem2  42640  aks5lem3a  42642  unitscyglem1  42648  rfovfvd  44447  rfovfvfvd  44448  rfovcnvf1od  44449  rfovcnvfvd  44452  fsovfvd  44455  fsovfvfvd  44456  fsovcnvlem  44458  dssmapfv2d  44463  dssmapfv3d  44464  dssmapnvod  44465  clsk3nimkb  44485  dvgrat  44757  radcnvrat  44759  hashnzfzclim  44767  binomcxplemnn0  44794  binomcxplemrat  44795  binomcxplemfrat  44796  binomcxplemradcnv  44797  binomcxplemcvg  44799  binomcxplemdvsum  44800  binomcxplemnotnn0  44801  mapss2  45652  fmuldfeqlem1  46030  clim1fr1  46049  climrec  46051  climexp  46053  climneg  46058  divcnvg  46075  sumnnodd  46078  supcnvlimsup  46186  icccncfext  46333  cncfioobdlem  46342  fprodsubrecnncnvlem  46353  fprodaddrecnncnvlem  46355  dvsinax  46359  fperdvper  46365  dvcosax  46372  ioodvbdlimc1lem2  46378  ioodvbdlimc2lem  46380  dvnmul  46389  dvnprodlem1  46392  dvnprodlem2  46393  dvnprodlem3  46394  itgsinexp  46401  itgcoscmulx  46415  itgsincmulx  46420  itgsubsticclem  46421  itgsubsticc  46422  itgiccshift  46426  wallispilem5  46515  wallispi  46516  wallispi2lem1  46517  wallispi2lem2  46518  wallispi2  46519  stirlinglem1  46520  stirlinglem2  46521  stirlinglem3  46522  stirlinglem4  46523  stirlinglem5  46524  stirlinglem7  46526  stirlinglem8  46527  stirlinglem10  46529  stirlinglem11  46530  stirlinglem12  46531  stirlinglem13  46532  stirlinglem14  46533  stirlinglem15  46534  dirkerval2  46540  dirkercncflem2  46550  fourierdlem7  46560  fourierdlem13  46566  fourierdlem14  46567  fourierdlem16  46569  fourierdlem18  46571  fourierdlem19  46572  fourierdlem21  46574  fourierdlem22  46575  fourierdlem26  46579  fourierdlem37  46590  fourierdlem39  46592  fourierdlem41  46594  fourierdlem48  46600  fourierdlem49  46601  fourierdlem50  46602  fourierdlem51  46603  fourierdlem53  46605  fourierdlem62  46614  fourierdlem63  46615  fourierdlem65  46617  fourierdlem73  46625  fourierdlem74  46626  fourierdlem75  46627  fourierdlem76  46628  fourierdlem79  46631  fourierdlem81  46633  fourierdlem82  46634  fourierdlem83  46635  fourierdlem84  46636  fourierdlem88  46640  fourierdlem89  46641  fourierdlem90  46642  fourierdlem91  46643  fourierdlem92  46644  fourierdlem93  46645  fourierdlem97  46649  fourierdlem101  46653  fourierdlem103  46655  fourierdlem104  46656  fourierdlem111  46663  fourierdlem112  46664  fouriersw  46677  elaa2lem  46679  etransclem13  46693  etransclem17  46697  etransclem18  46698  etransclem21  46701  etransclem31  46711  etransclem32  46712  etransclem33  46713  etransclem35  46715  etransclem46  46726  etransclem48  46728  rrxtopnfi  46733  salgenval  46767  sge0val  46812  sge0z  46821  sge0snmpt  46829  sge0xp  46875  nnfoctbdjlem  46901  omeiunltfirp  46965  caratheodorylem1  46972  0ome  46975  ovnval2  46991  hoicvr  46994  ovncvrrp  47010  ovn0lem  47011  ovnsubaddlem1  47016  hsphoif  47022  hsphoival  47025  hoidmv1le  47040  hoidmvlelem3  47043  ovnhoilem2  47048  ovncvr2  47057  hoidifhspval2  47061  hoidifhspval3  47065  hspmbllem2  47073  smfid  47198  fsetsnf1  47512  fsetsnfo  47513  cfsetsnfsetfv  47517  cfsetsnfsetfo  47520  fvmptrab  47752  fundcmpsurinjlem3  47872  sprval  47951  prproropreud  47981  upgrimwlklem3  48387  grtri  48428  stgrfv  48441  isubgr3stgrlem5  48458  rngcvalALTV  48753  rngcidALTV  48762  rhmsubcALTVlem3  48771  ringcvalALTV  48777  funcringcsetcALTV2lem1  48778  ringcidALTV  48796  funcringcsetclem1ALTV  48801  scmsuppss  48859  ply1mulgsum  48878  lindslinindsimp1  48945  lindsrng01  48956  islindeps2  48971  fdivmptfv  49033  refdivmptfv  49034  1arympt1fv  49127  itcoval0  49150  itcoval1  49151  itcoval2  49152  itcoval3  49153  itcovalsuc  49155  ackvalsuc1mpt  49166  ackvalsuc1  49167  ackval1  49169  ackval2  49170  ackval3  49171  ackval0val  49174  swapf1a  49756  swapf2a  49758  swapf1  49759  swapf2  49761  tposcurf2val  49788  fuco23  49828  prcof1  49875  prcof21a  49878  mndtcid  50076  amgmwlem  50289