Theorem fvmptd 7002

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144   ↦ cmpt 5185  ‘cfv 6539

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-iota 6494  df-fun 6541  df-fv 6547

This theorem is used by:  fvmptd2  7003  fvmptdv2  7013  fvmptd4  7019  mptcnfimad  7999  fsplitfpar  8132  mpocurryvald  8291  ttukeylem3  10593  indval  12327  indfval  12331  tpf1ofv0  14645  tpf1ofv1  14646  tpf1ofv2  14647  ccatval1  14726  ccatval2  14727  repswsymb  14930  relexp1g  15185  rtrclreclem1  15216  rtrclreclem4  15220  dfrtrcl2  15221  prmodvdslcmf  17231  prmgap  17243  prmgaplcm  17244  prmgapprmo  17246  prdsvscafval  17657  mrcval  17790  cidval  17857  subcid  18028  idfu2nd  18058  resf2nd  18076  fuccoval  18147  fucid  18155  homaval  18212  idaval  18239  setcid  18267  catcid  18288  estrcid  18314  funcestrcsetclem1  18320  funcsetcestrclem1  18334  prf1  18380  prf2  18382  curf1  18405  curf11  18406  curf2val  18410  hof2  18437  yonedalem4a  18455  vrmdval  19059  smndex1gbasOLD  19105  smndex1gid  19106  smndex1gidOLD  19107  smndex1n0mnd  19117  mulgnngsum  19295  pj1val  19915  dpjval  20278  c0mgm  20695  c0mhm  20696  c0snmgmhm  20698  c0snmhm  20699  zrrnghm  20794  zrinitorngc  20900  zrtermorngc  20901  zrtermoringc  20933  sraval  21456  rngqiprngimfv  21600  frlmphl  22093  opsrval  22361  selvfval  22434  mhpval  22466  mhpsclcl  22474  psdfval  22485  cply1mul  22620  cply1coe0  22625  cply1coe0bi  22626  gsummoncoe1  22632  evls1sca  22647  mvmulfv  22865  mavmulfv  22867  mdetuni0  22942  mat2pmatval  23048  m2cpm  23065  cpm2mval  23074  m2cpminvid2lem  23078  decpmatid  23094  decpmatmullem  23095  pmatcollpw2lem  23101  monmatcollpw  23103  pm2mpfval  23120  mp2pm2mplem4  23133  pm2mpmhmlem2  23143  chpmatval  23155  fcfval  24358  cnextfval  24387  utopsnneiplem  24572  rrxmvallem  25731  rrxmval  25732  itgpowd  26376  taylpval  26700  lgamgulmlem2  27363  lgamcvglem  27373  logexprlim  27558  dchr1  27590  ishlg  29074  mirval  29133  mirfv  29134  ishpg  29243  lmif  29296  islmib  29298  lmodvslmhm  33658  psgnfzto1stlem  33708  tocycfv  33717  sgnsval  33769  psrnzr  34191  0mplrim  34193  selvply1rhmlemb  34198  selvply1rhmlem2  34200  mplvrpmrhm  34226  esplyfval0  34243  esplyind  34254  evls1fldgencl  34349  minplyval  34384  rtelextdg2lem  34405  2sqr3minply  34459  cos9thpiminply  34467  zarcls0  34547  zarcls1  34548  zarclsiin  34550  zarclsint  34551  zarclssn  34552  qqhvval  34662  esummulc1  34760  esumcvg  34765  ofcval  34778  sigagenval  34820  measinb  34901  omsfval  34973  omssubadd  34979  sitgfval  35020  eulerpartlemsv1  35035  eulerpartlems  35039  fibp1  35080  totprobd  35105  probmeasb  35109  dstrvprob  35151  dstfrvinc  35156  dstfrvclim1  35157  ballotlemfval  35169  ballotlemsv  35189  gsumnunsn  35220  signsply0  35227  signstfval  35240  fdvneggt  35276  fdvnegge  35278  itgexpif  35282  breprexplema  35306  vtsval  35313  logdivsqrle  35326  hgt750lemg  35330  afsval  35350  lpadval  35355  cvmliftlem9  36145  goel  36199  satf0suc  36228  sat1el2xp  36231  fmlafv  36232  fmla  36233  fmlasuc0  36236  ex-sategoelel  36273  ex-sategoelelomsuc  36278  mvrsval  36357  mrsubfval  36360  mrsubval  36361  msubfval  36376  msubval  36377  msrval  36390  fwddifval  37020  fwddifnval  37021  knoppcnlem1  37452  knoppcnlem4  37455  knoppcnlem6  37457  knoppcnlem7  37458  bj-imdirval2  38198  bj-iminvval2  38209  bj-fvmptunsn2  38273  bj-endval  38330  poimirlem1  38633  poimirlem2  38634  poimirlem5  38637  poimirlem6  38638  poimirlem7  38639  poimirlem10  38642  poimirlem11  38643  poimirlem12  38644  poimirlem19  38651  poimirlem22  38654  mblfinlem2  38670  areacirc  38725  tendopl2  41928  tendoi2  41946  erngplus2  41955  erngplus2-rN  41963  hlhilset  43085  rhmzrhval  43116  lcmineqlem12  43184  aks4d1p9  43232  primrootscoprbij  43246  aks6d1c1p3  43254  aks6d1c1p5  43256  aks6d1c1  43260  hashscontpow  43266  aks6d1c3  43267  aks6d1c4  43268  aks6d1c2lem4  43271  aks6d1c2  43274  aks6d1c5lem3  43281  deg1gprod  43284  sticksstones2  43291  sticksstones3  43292  sticksstones6  43295  sticksstones7  43296  sticksstones8  43297  sticksstones10  43299  sticksstones12a  43301  sticksstones12  43302  sticksstones17  43307  sticksstones18  43308  sticksstones19  43309  aks6d1c6lem1  43314  aks6d1c6lem2  43315  aks6d1c6lem3  43316  aks6d1c6lem4  43317  aks6d1c6isolem1  43318  aks6d1c6isolem2  43319  aks6d1c6isolem3  43320  aks6d1c6lem5  43321  aks6d1c7lem1  43324  aks5lem2  43331  aks5lem3a  43333  unitscyglem1  43339  rfovfvd  45096  rfovfvfvd  45097  rfovcnvf1od  45098  rfovcnvfvd  45101  fsovfvd  45104  fsovfvfvd  45105  fsovcnvlem  45107  dssmapfv2d  45112  dssmapfv3d  45113  dssmapnvod  45114  clsk3nimkb  45134  dvgrat  45390  radcnvrat  45392  hashnzfzclim  45400  binomcxplemnn0  45427  binomcxplemrat  45428  binomcxplemfrat  45429  binomcxplemradcnv  45430  binomcxplemcvg  45432  binomcxplemdvsum  45433  binomcxplemnotnn0  45434  mapss2  46313  fmuldfeqlem1  46688  clim1fr1  46707  climrec  46709  climexp  46711  climneg  46716  divcnvg  46733  supcnvlimsup  46844  icccncfext  46991  cncfioobdlem  47000  fprodsubrecnncnvlem  47011  fprodaddrecnncnvlem  47013  dvsinax  47017  fperdvper  47023  dvcosax  47030  ioodvbdlimc1lem2  47036  ioodvbdlimc2lem  47038  dvnmul  47047  dvnprodlem1  47050  dvnprodlem2  47051  dvnprodlem3  47052  itgsinexp  47059  itgcoscmulx  47073  itgsincmulx  47078  itgsubsticclem  47079  itgsubsticc  47080  itgiccshift  47084  wallispilem5  47173  wallispi  47174  wallispi2lem1  47175  wallispi2lem2  47176  wallispi2  47177  stirlinglem1  47178  stirlinglem2  47179  stirlinglem3  47180  stirlinglem4  47181  stirlinglem5  47182  stirlinglem7  47184  stirlinglem8  47185  stirlinglem10  47187  stirlinglem11  47188  stirlinglem12  47189  stirlinglem13  47190  stirlinglem14  47191  stirlinglem15  47192  dirkerval2  47198  dirkercncflem2  47208  fourierdlem7  47218  fourierdlem13  47224  fourierdlem14  47225  fourierdlem16  47227  fourierdlem18  47229  fourierdlem19  47230  fourierdlem21  47232  fourierdlem22  47233  fourierdlem26  47237  fourierdlem37  47248  fourierdlem39  47250  fourierdlem41  47252  fourierdlem50  47260  fourierdlem51  47261  fourierdlem53  47263  fourierdlem62  47272  fourierdlem63  47273  fourierdlem65  47275  fourierdlem73  47283  fourierdlem74  47284  fourierdlem75  47285  fourierdlem76  47286  fourierdlem79  47289  fourierdlem81  47291  fourierdlem82  47292  fourierdlem83  47293  fourierdlem84  47294  fourierdlem88  47298  fourierdlem89  47299  fourierdlem90  47300  fourierdlem91  47301  fourierdlem92  47302  fourierdlem93  47303  fourierdlem97  47307  fourierdlem101  47311  fourierdlem103  47313  fourierdlem104  47314  fourierdlem111  47321  fourierdlem112  47322  fouriersw  47335  elaa2lem  47337  etransclem13  47351  etransclem17  47355  etransclem18  47356  etransclem21  47359  etransclem31  47369  etransclem32  47370  etransclem33  47371  etransclem35  47373  etransclem46  47384  etransclem48  47386  rrxtopnfi  47391  salgenval  47425  sge0val  47470  sge0z  47479  sge0snmpt  47487  sge0xp  47533  nnfoctbdjlem  47559  omeiunltfirp  47623  caratheodorylem1  47630  0ome  47633  ovnval2  47649  hoicvr  47652  ovncvrrp  47668  ovn0lem  47669  ovnsubaddlem1  47674  hsphoif  47680  hsphoival  47683  hoidmv1le  47698  hoidmvlelem3  47701  ovnhoilem2  47706  ovncvr2  47715  hoidifhspval2  47719  hoidifhspval3  47723  hspmbllem2  47731  smfid  47856  fsetsnf1  48216  fsetsnfo  48217  cfsetsnfsetfv  48221  cfsetsnfsetfo  48224  fvmptrab  48456  fundcmpsurinjlem3  48576  sprval  48655  prproropreud  48685  upgrimwlklem3  49091  grtri  49132  stgrfv  49145  isubgr3stgrlem5  49162  rngcvalALTV  49456  rngcidALTV  49465  rhmsubcALTVlem3  49474  ringcvalALTV  49480  funcringcsetcALTV2lem1  49481  ringcidALTV  49499  funcringcsetclem1ALTV  49504  scmsuppss  49577  ply1mulgsum  49596  lindslinindsimp1  49663  lindsrng01  49674  islindeps2  49689  fdivmptfv  49751  refdivmptfv  49752  1arympt1fv  49845  itcoval0  49868  itcoval1  49869  itcoval2  49870  itcoval3  49871  itcovalsuc  49873  ackvalsuc1mpt  49884  ackvalsuc1  49885  ackval1  49887  ackval2  49888  ackval3  49889  ackval0val  49892  fvmpomptd  50077  swapf1a  50485  swapf2a  50487  swapf1  50488  swapf2  50490  tposcurf2val  50517  fuco23  50557  postcof2  50594  prcof1  50617  prcof21a  50620  mndtcid  50821  veronesev1lem  51142  veronesev2lem  51143  veronesev3lem  51144  veronesev4lem  51145  veronesev5lem  51146  veronesev6lem  51147  amgmwlem  51156