Theorem fvmptd 7001

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1568   ∈ wcel 2150   ↦ cmpt 5197  ‘cfv 6540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2152  ax-9 2160  ax-10 2183  ax-11 2199  ax-12 2220  ax-ext 2742  ax-sep 5262  ax-pr 5408

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-nf 1812  df-sb 2099  df-mo 2574  df-eu 2604  df-clab 2749  df-cleq 2762  df-clel 2845  df-nfc 2919  df-ral 3087  df-rex 3097  df-rab 3424  df-v 3464  df-sbc 3753  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5560  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-iota 6496  df-fun 6542  df-fv 6548

This theorem is referenced by:  fvmptd2  7002  fvmptdv2  7012  fvmptd4  7018  mptcnfimad  7986  fsplitfpar  8116  mpocurryvald  8269  ttukeylem3  10498  indval  12224  indfval  12228  tpf1ofv0  14536  tpf1ofv1  14537  tpf1ofv2  14538  ccatval1  14617  ccatval2  14618  repswsymb  14814  relexp1g  15066  rtrclreclem1  15097  rtrclreclem4  15101  dfrtrcl2  15102  prmodvdslcmf  17110  prmgap  17122  prmgaplcm  17123  prmgapprmo  17125  prdsvscafval  17536  mrcval  17669  cidval  17736  subcid  17907  idfu2nd  17937  resf2nd  17955  fuccoval  18026  fucid  18034  homaval  18091  idaval  18118  setcid  18146  catcid  18167  estrcid  18193  funcestrcsetclem1  18199  funcsetcestrclem1  18213  prf1  18259  prf2  18261  curf1  18284  curf11  18285  curf2val  18289  hof2  18316  yonedalem4a  18334  vrmdval  18919  smndex1gbasOLD  18965  smndex1gid  18966  smndex1gidOLD  18967  smndex1n0mnd  18977  mulgnngsum  19148  pj1val  19768  dpjval  20131  c0mgm  20544  c0mhm  20545  c0snmgmhm  20547  c0snmhm  20548  zrrnghm  20624  zrinitorngc  20730  zrtermorngc  20731  zrtermoringc  20763  sraval  21279  rngqiprngimfv  21421  frlmphl  21914  opsrval  22180  selvfval  22253  mhpval  22285  mhpsclcl  22293  psdfval  22304  cply1mul  22439  cply1coe0  22444  cply1coe0bi  22445  gsummoncoe1  22451  evls1sca  22466  mvmulfv  22684  mavmulfv  22686  mdetuni0  22761  mat2pmatval  22864  m2cpm  22881  cpm2mval  22890  m2cpminvid2lem  22894  decpmatid  22910  decpmatmullem  22911  pmatcollpw2lem  22917  monmatcollpw  22919  pm2mpfval  22936  mp2pm2mplem4  22949  pm2mpmhmlem2  22959  chpmatval  22971  fcfval  24173  cnextfval  24202  utopsnneiplem  24387  rrxmvallem  25546  rrxmval  25547  itgpowd  26192  taylpval  26510  lgamgulmlem2  27174  lgamcvglem  27184  logexprlim  27369  dchr1  27401  ishlg  28854  mirval  28912  mirfv  28913  ishpg  29020  lmif  29072  islmib  29074  lmodvslmhm  33340  psgnfzto1stlem  33390  tocycfv  33399  sgnsval  33451  psrnzr  33872  0mplrim  33874  selvply1rhmlemb  33879  selvply1rhmlem2  33881  mplvrpmrhm  33907  esplyfval0  33924  esplyind  33935  evls1fldgencl  34030  minplyval  34065  rtelextdg2lem  34086  2sqr3minply  34140  cos9thpiminply  34148  zarcls0  34228  zarcls1  34229  zarclsiin  34231  zarclsint  34232  zarclssn  34233  qqhvval  34343  esummulc1  34441  esumcvg  34446  ofcval  34459  sigagenval  34500  measinb  34581  omsfval  34654  omssubadd  34660  sitgfval  34701  eulerpartlemsv1  34716  eulerpartlems  34720  fibp1  34761  totprobd  34786  probmeasb  34790  dstrvprob  34832  dstfrvinc  34837  dstfrvclim1  34838  ballotlemfval  34850  ballotlemsv  34870  gsumnunsn  34901  signsply0  34908  signstfval  34921  fdvneggt  34957  fdvnegge  34959  itgexpif  34963  breprexplema  34987  vtsval  34994  logdivsqrle  35007  hgt750lemg  35011  afsval  35031  lpadval  35036  cvmliftlem9  35743  goel  35797  satf0suc  35826  sat1el2xp  35829  fmlafv  35830  fmla  35831  fmlasuc0  35834  ex-sategoelel  35871  ex-sategoelelomsuc  35876  mvrsval  35955  mrsubfval  35958  mrsubval  35959  msubfval  35974  msubval  35975  msrval  35988  fwddifval  36612  fwddifnval  36613  knoppcnlem1  37030  knoppcnlem4  37033  knoppcnlem6  37035  knoppcnlem7  37036  bj-imdirval2  37775  bj-iminvval2  37786  bj-fvmptunsn2  37850  bj-endval  37907  poimirlem1  38220  poimirlem2  38221  poimirlem5  38224  poimirlem6  38225  poimirlem7  38226  poimirlem10  38229  poimirlem11  38230  poimirlem12  38231  poimirlem19  38238  poimirlem22  38241  mblfinlem2  38257  areacirc  38312  tendopl2  41501  tendoi2  41519  erngplus2  41528  erngplus2-rN  41536  hlhilset  42658  rhmzrhval  42689  lcmineqlem12  42757  aks4d1p9  42805  primrootscoprbij  42819  aks6d1c1p3  42827  aks6d1c1p5  42829  aks6d1c1  42833  hashscontpow  42839  aks6d1c3  42840  aks6d1c4  42841  aks6d1c2lem4  42844  aks6d1c2  42847  aks6d1c5lem3  42854  deg1gprod  42857  sticksstones2  42864  sticksstones3  42865  sticksstones6  42868  sticksstones7  42869  sticksstones8  42870  sticksstones10  42872  sticksstones12a  42874  sticksstones12  42875  sticksstones17  42880  sticksstones18  42881  sticksstones19  42882  aks6d1c6lem1  42887  aks6d1c6lem2  42888  aks6d1c6lem3  42889  aks6d1c6lem4  42890  aks6d1c6isolem1  42891  aks6d1c6isolem2  42892  aks6d1c6isolem3  42893  aks6d1c6lem5  42894  aks6d1c7lem1  42897  aks5lem2  42904  aks5lem3a  42906  unitscyglem1  42912  rfovfvd  44680  rfovfvfvd  44681  rfovcnvf1od  44682  rfovcnvfvd  44685  fsovfvd  44688  fsovfvfvd  44689  fsovcnvlem  44691  dssmapfv2d  44696  dssmapfv3d  44697  dssmapnvod  44698  clsk3nimkb  44718  dvgrat  44974  radcnvrat  44976  hashnzfzclim  44984  binomcxplemnn0  45011  binomcxplemrat  45012  binomcxplemfrat  45013  binomcxplemradcnv  45014  binomcxplemcvg  45016  binomcxplemdvsum  45017  binomcxplemnotnn0  45018  mapss2  45874  fmuldfeqlem1  46250  clim1fr1  46269  climrec  46271  climexp  46273  climneg  46278  divcnvg  46295  sumnnodd  46298  supcnvlimsup  46406  icccncfext  46553  cncfioobdlem  46562  fprodsubrecnncnvlem  46573  fprodaddrecnncnvlem  46575  dvsinax  46579  fperdvper  46585  dvcosax  46592  ioodvbdlimc1lem2  46598  ioodvbdlimc2lem  46600  dvnmul  46609  dvnprodlem1  46612  dvnprodlem2  46613  dvnprodlem3  46614  itgsinexp  46621  itgcoscmulx  46635  itgsincmulx  46640  itgsubsticclem  46641  itgsubsticc  46642  itgiccshift  46646  wallispilem5  46735  wallispi  46736  wallispi2lem1  46737  wallispi2lem2  46738  wallispi2  46739  stirlinglem1  46740  stirlinglem2  46741  stirlinglem3  46742  stirlinglem4  46743  stirlinglem5  46744  stirlinglem7  46746  stirlinglem8  46747  stirlinglem10  46749  stirlinglem11  46750  stirlinglem12  46751  stirlinglem13  46752  stirlinglem14  46753  stirlinglem15  46754  dirkerval2  46760  dirkercncflem2  46770  fourierdlem7  46780  fourierdlem13  46786  fourierdlem14  46787  fourierdlem16  46789  fourierdlem18  46791  fourierdlem19  46792  fourierdlem21  46794  fourierdlem22  46795  fourierdlem26  46799  fourierdlem37  46810  fourierdlem39  46812  fourierdlem41  46814  fourierdlem50  46822  fourierdlem51  46823  fourierdlem53  46825  fourierdlem62  46834  fourierdlem63  46835  fourierdlem65  46837  fourierdlem73  46845  fourierdlem74  46846  fourierdlem75  46847  fourierdlem76  46848  fourierdlem79  46851  fourierdlem81  46853  fourierdlem82  46854  fourierdlem83  46855  fourierdlem84  46856  fourierdlem88  46860  fourierdlem89  46861  fourierdlem90  46862  fourierdlem91  46863  fourierdlem92  46864  fourierdlem93  46865  fourierdlem97  46869  fourierdlem101  46873  fourierdlem103  46875  fourierdlem104  46876  fourierdlem111  46883  fourierdlem112  46884  fouriersw  46897  elaa2lem  46899  etransclem13  46913  etransclem17  46917  etransclem18  46918  etransclem21  46921  etransclem31  46931  etransclem32  46932  etransclem33  46933  etransclem35  46935  etransclem46  46946  etransclem48  46948  rrxtopnfi  46953  salgenval  46987  sge0val  47032  sge0z  47041  sge0snmpt  47049  sge0xp  47095  nnfoctbdjlem  47121  omeiunltfirp  47185  caratheodorylem1  47192  0ome  47195  ovnval2  47211  hoicvr  47214  ovncvrrp  47230  ovn0lem  47231  ovnsubaddlem1  47236  hsphoif  47242  hsphoival  47245  hoidmv1le  47260  hoidmvlelem3  47263  ovnhoilem2  47268  ovncvr2  47277  hoidifhspval2  47281  hoidifhspval3  47285  hspmbllem2  47293  smfid  47418  fsetsnf1  47738  fsetsnfo  47739  cfsetsnfsetfv  47743  cfsetsnfsetfo  47746  fvmptrab  47978  fundcmpsurinjlem3  48098  sprval  48177  prproropreud  48207  upgrimwlklem3  48613  grtri  48654  stgrfv  48667  isubgr3stgrlem5  48684  rngcvalALTV  48979  rngcidALTV  48988  rhmsubcALTVlem3  48997  ringcvalALTV  49003  funcringcsetcALTV2lem1  49004  ringcidALTV  49022  funcringcsetclem1ALTV  49027  scmsuppss  49100  ply1mulgsum  49119  lindslinindsimp1  49186  lindsrng01  49197  islindeps2  49212  fdivmptfv  49274  refdivmptfv  49275  1arympt1fv  49368  itcoval0  49391  itcoval1  49392  itcoval2  49393  itcoval3  49394  itcovalsuc  49396  ackvalsuc1mpt  49407  ackvalsuc1  49408  ackval1  49410  ackval2  49411  ackval3  49412  ackval0val  49415  swapf1a  49996  swapf2a  49998  swapf1  49999  swapf2  50001  tposcurf2val  50028  fuco23  50068  prcof1  50115  prcof21a  50118  mndtcid  50316  amgmwlem  50551