Theorem fvmptd 6978

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

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

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-iota 6467  df-fun 6516  df-fv 6522

This theorem is referenced by:  fvmptd2  6979  fvmptdv2  6989  fvmptd4  6995  mptcnfimad  7968  fsplitfpar  8100  mpocurryvald  8252  ttukeylem3  10471  tpf1ofv0  14468  tpf1ofv1  14469  tpf1ofv2  14470  ccatval1  14549  ccatval2  14550  repswsymb  14746  relexp1g  14999  rtrclreclem1  15030  rtrclreclem4  15034  dfrtrcl2  15035  prmodvdslcmf  17025  prmgap  17037  prmgaplcm  17038  prmgapprmo  17040  prdsvscafval  17450  mrcval  17578  cidval  17645  subcid  17816  idfu2nd  17846  resf2nd  17864  fuccoval  17935  fucid  17943  homaval  18000  idaval  18027  setcid  18055  catcid  18076  estrcid  18102  funcestrcsetclem1  18108  funcsetcestrclem1  18122  prf1  18168  prf2  18170  curf1  18193  curf11  18194  curf2val  18198  hof2  18225  yonedalem4a  18243  vrmdval  18791  smndex1gbas  18836  smndex1gid  18837  smndex1n0mnd  18846  mulgnngsum  19018  pj1val  19632  dpjval  19995  c0mgm  20375  c0mhm  20376  c0snmgmhm  20378  c0snmhm  20379  zrrnghm  20452  zrinitorngc  20558  zrtermorngc  20559  zrtermoringc  20591  sraval  21089  rngqiprngimfv  21215  frlmphl  21697  opsrval  21960  selvfval  22028  mhpval  22033  mhpsclcl  22041  psdfval  22052  cply1mul  22190  cply1coe0  22195  cply1coe0bi  22196  gsummoncoe1  22202  evls1sca  22217  mvmulfv  22438  mavmulfv  22440  mdetuni0  22515  mat2pmatval  22618  m2cpm  22635  cpm2mval  22644  m2cpminvid2lem  22648  decpmatid  22664  decpmatmullem  22665  pmatcollpw2lem  22671  monmatcollpw  22673  pm2mpfval  22690  mp2pm2mplem4  22703  pm2mpmhmlem2  22713  chpmatval  22725  fcfval  23927  cnextfval  23956  utopsnneiplem  24142  rrxmvallem  25311  rrxmval  25312  itgpowd  25964  taylpval  26281  lgamgulmlem2  26947  lgamcvglem  26957  logexprlim  27143  dchr1  27175  ishlg  28536  mirval  28589  mirfv  28590  ishpg  28693  lmif  28719  islmib  28721  indval  32783  indfval  32786  lmodvslmhm  32997  psgnfzto1stlem  33064  tocycfv  33073  sgnsval  33125  evls1fldgencl  33672  minplyval  33702  rtelextdg2lem  33723  2sqr3minply  33777  cos9thpiminply  33785  zarcls0  33865  zarcls1  33866  zarclsiin  33868  zarclsint  33869  zarclssn  33870  qqhvval  33980  esummulc1  34078  esumcvg  34083  ofcval  34096  sigagenval  34137  measinb  34218  omsfval  34292  omssubadd  34298  sitgfval  34339  eulerpartlemsv1  34354  eulerpartlems  34358  fibp1  34399  totprobd  34424  probmeasb  34428  dstrvprob  34470  dstfrvinc  34475  dstfrvclim1  34476  ballotlemfval  34488  ballotlemsv  34508  gsumnunsn  34539  signsply0  34549  signstfval  34562  fdvneggt  34598  fdvnegge  34600  itgexpif  34604  breprexplema  34628  vtsval  34635  logdivsqrle  34648  hgt750lemg  34652  afsval  34669  lpadval  34674  cvmliftlem9  35287  goel  35341  satf0suc  35370  sat1el2xp  35373  fmlafv  35374  fmla  35375  fmlasuc0  35378  ex-sategoelel  35415  ex-sategoelelomsuc  35420  mvrsval  35499  mrsubfval  35502  mrsubval  35503  msubfval  35518  msubval  35519  msrval  35532  fwddifval  36157  fwddifnval  36158  knoppcnlem1  36488  knoppcnlem4  36491  knoppcnlem6  36493  knoppcnlem7  36494  bj-imdirval2  37178  bj-iminvval2  37189  bj-fvmptunsn2  37253  bj-endval  37310  poimirlem1  37622  poimirlem2  37623  poimirlem5  37626  poimirlem6  37627  poimirlem7  37628  poimirlem10  37631  poimirlem11  37632  poimirlem12  37633  poimirlem19  37640  poimirlem22  37643  mblfinlem2  37659  areacirc  37714  tendopl2  40778  tendoi2  40796  erngplus2  40805  erngplus2-rN  40813  hlhilset  41935  rhmzrhval  41966  lcmineqlem12  42035  aks4d1p9  42083  primrootscoprbij  42097  aks6d1c1p3  42105  aks6d1c1p5  42107  aks6d1c1  42111  hashscontpow  42117  aks6d1c3  42118  aks6d1c4  42119  aks6d1c2lem4  42122  aks6d1c2  42125  aks6d1c5lem3  42132  deg1gprod  42135  sticksstones2  42142  sticksstones3  42143  sticksstones6  42146  sticksstones7  42147  sticksstones8  42148  sticksstones10  42150  sticksstones12a  42152  sticksstones12  42153  sticksstones17  42158  sticksstones18  42159  sticksstones19  42160  aks6d1c6lem1  42165  aks6d1c6lem2  42166  aks6d1c6lem3  42167  aks6d1c6lem4  42168  aks6d1c6isolem1  42169  aks6d1c6isolem2  42170  aks6d1c6isolem3  42171  aks6d1c6lem5  42172  aks6d1c7lem1  42175  aks5lem2  42182  aks5lem3a  42184  unitscyglem1  42190  rfovfvd  43998  rfovfvfvd  43999  rfovcnvf1od  44000  rfovcnvfvd  44003  fsovfvd  44006  fsovfvfvd  44007  fsovcnvlem  44009  dssmapfv2d  44014  dssmapfv3d  44015  dssmapnvod  44016  clsk3nimkb  44036  dvgrat  44308  radcnvrat  44310  hashnzfzclim  44318  binomcxplemnn0  44345  binomcxplemrat  44346  binomcxplemfrat  44347  binomcxplemradcnv  44348  binomcxplemcvg  44350  binomcxplemdvsum  44351  binomcxplemnotnn0  44352  mapss2  45206  fmuldfeqlem1  45587  clim1fr1  45606  climrec  45608  climexp  45610  climneg  45615  divcnvg  45632  sumnnodd  45635  supcnvlimsup  45745  icccncfext  45892  cncfioobdlem  45901  fprodsubrecnncnvlem  45912  fprodaddrecnncnvlem  45914  dvsinax  45918  fperdvper  45924  dvcosax  45931  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  dvnmul  45948  dvnprodlem1  45951  dvnprodlem2  45952  dvnprodlem3  45953  itgsinexp  45960  itgcoscmulx  45974  itgsincmulx  45979  itgsubsticclem  45980  itgsubsticc  45981  itgiccshift  45985  wallispilem5  46074  wallispi  46075  wallispi2lem1  46076  wallispi2lem2  46077  wallispi2  46078  stirlinglem1  46079  stirlinglem2  46080  stirlinglem3  46081  stirlinglem4  46082  stirlinglem5  46083  stirlinglem7  46085  stirlinglem8  46086  stirlinglem10  46088  stirlinglem11  46089  stirlinglem12  46090  stirlinglem13  46091  stirlinglem14  46092  stirlinglem15  46093  dirkerval2  46099  dirkercncflem2  46109  fourierdlem7  46119  fourierdlem13  46125  fourierdlem14  46126  fourierdlem16  46128  fourierdlem18  46130  fourierdlem19  46131  fourierdlem21  46133  fourierdlem22  46134  fourierdlem26  46138  fourierdlem37  46149  fourierdlem39  46151  fourierdlem41  46153  fourierdlem48  46159  fourierdlem49  46160  fourierdlem50  46161  fourierdlem51  46162  fourierdlem53  46164  fourierdlem62  46173  fourierdlem63  46174  fourierdlem65  46176  fourierdlem73  46184  fourierdlem74  46185  fourierdlem75  46186  fourierdlem76  46187  fourierdlem79  46190  fourierdlem81  46192  fourierdlem82  46193  fourierdlem83  46194  fourierdlem84  46195  fourierdlem88  46199  fourierdlem89  46200  fourierdlem90  46201  fourierdlem91  46202  fourierdlem92  46203  fourierdlem93  46204  fourierdlem97  46208  fourierdlem101  46212  fourierdlem103  46214  fourierdlem104  46215  fourierdlem111  46222  fourierdlem112  46223  fouriersw  46236  elaa2lem  46238  etransclem13  46252  etransclem17  46256  etransclem18  46257  etransclem21  46260  etransclem31  46270  etransclem32  46271  etransclem33  46272  etransclem35  46274  etransclem46  46285  etransclem48  46287  rrxtopnfi  46292  salgenval  46326  sge0val  46371  sge0z  46380  sge0snmpt  46388  sge0xp  46434  nnfoctbdjlem  46460  omeiunltfirp  46524  caratheodorylem1  46531  0ome  46534  ovnval2  46550  hoicvr  46553  ovncvrrp  46569  ovn0lem  46570  ovnsubaddlem1  46575  hsphoif  46581  hsphoival  46584  hoidmv1le  46599  hoidmvlelem3  46602  ovnhoilem2  46607  ovncvr2  46616  hoidifhspval2  46620  hoidifhspval3  46624  hspmbllem2  46632  smfid  46757  fsetsnf1  47057  fsetsnfo  47058  cfsetsnfsetfv  47062  cfsetsnfsetfo  47065  fvmptrab  47297  fundcmpsurinjlem3  47405  sprval  47484  prproropreud  47514  upgrimwlklem3  47903  grtri  47943  stgrfv  47956  isubgr3stgrlem5  47973  rngcvalALTV  48257  rngcidALTV  48266  rhmsubcALTVlem3  48275  ringcvalALTV  48281  funcringcsetcALTV2lem1  48282  ringcidALTV  48300  funcringcsetclem1ALTV  48305  scmsuppss  48363  ply1mulgsum  48383  lindslinindsimp1  48450  lindsrng01  48461  islindeps2  48476  fdivmptfv  48538  refdivmptfv  48539  1arympt1fv  48632  itcoval0  48655  itcoval1  48656  itcoval2  48657  itcoval3  48658  itcovalsuc  48660  ackvalsuc1mpt  48671  ackvalsuc1  48672  ackval1  48674  ackval2  48675  ackval3  48676  ackval0val  48679  swapf1a  49262  swapf2a  49264  swapf1  49265  swapf2  49267  tposcurf2val  49294  fuco23  49334  prcof1  49381  prcof21a  49384  mndtcid  49582  amgmwlem  49795