Theorem fvmptd 7030

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2147   ↦ cmpt 5190  ‘cfv 6564

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5253  ax-pr 5396

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5172  df-mpt 5191  df-id 5551  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-iota 6518  df-fun 6566  df-fv 6572

This theorem is used by:  fvmptd2  7031  fvmptdv2  7041  fvmptd4  7047  mptcnfimad  8030  fsplitfpar  8164  mpocurryvald  8323  ttukeylem3  10626  indval  12361  indfval  12365  tpf1ofv0  14680  tpf1ofv1  14681  tpf1ofv2  14682  ccatval1  14761  ccatval2  14762  repswsymb  14965  relexp1g  15220  rtrclreclem1  15251  rtrclreclem4  15255  dfrtrcl2  15256  prmodvdslcmf  17266  prmgap  17278  prmgaplcm  17279  prmgapprmo  17281  prdsvscafval  17692  mrcval  17825  cidval  17892  subcid  18063  idfu2nd  18093  resf2nd  18111  fuccoval  18182  fucid  18190  homaval  18247  idaval  18274  setcid  18302  catcid  18323  estrcid  18349  funcestrcsetclem1  18355  funcsetcestrclem1  18369  prf1  18415  prf2  18417  curf1  18440  curf11  18441  curf2val  18445  hof2  18472  yonedalem4a  18490  vrmdval  19094  smndex1gbasOLD  19140  smndex1gid  19141  smndex1gidOLD  19142  smndex1n0mnd  19152  mulgnngsum  19330  pj1val  19951  dpjval  20314  c0mgm  20731  c0mhm  20732  c0snmgmhm  20734  c0snmhm  20735  zrrnghm  20830  zrinitorngc  20936  zrtermorngc  20937  zrtermoringc  20969  sraval  21492  rngqiprngimfv  21636  frlmphl  22131  opsrval  22399  selvfval  22472  mhpval  22504  mhpsclcl  22512  psdfval  22523  cply1mul  22658  cply1coe0  22663  cply1coe0bi  22664  gsummoncoe1  22670  evls1sca  22685  mvmulfv  22903  mavmulfv  22905  mdetuni0  22980  mat2pmatval  23086  m2cpm  23103  cpm2mval  23112  m2cpminvid2lem  23116  decpmatid  23132  decpmatmullem  23133  pmatcollpw2lem  23139  monmatcollpw  23141  pm2mpfval  23158  mp2pm2mplem4  23171  pm2mpmhmlem2  23181  chpmatval  23193  fcfval  24396  cnextfval  24425  utopsnneiplem  24610  rrxmvallem  25769  rrxmval  25770  itgpowd  26414  taylpval  26740  lgamgulmlem2  27403  lgamcvglem  27413  logexprlim  27598  dchr1  27630  ishlg  29114  mirval  29173  mirfv  29174  ishpg  29283  lmif  29336  islmib  29338  lmodvslmhm  33700  psgnfzto1stlem  33750  tocycfv  33759  sgnsval  33811  rngunsnply1chr2lem2  34244  psrnzr  34248  0mplrim  34250  selvply1rhmlemb  34255  selvply1rhmlem2  34257  mplvrpmrhm  34283  esplyfval0  34300  esplyind  34311  evls1fldgencl  34406  minplyval  34441  rtelextdg2lem  34462  2sqr3minply  34516  cos9thpiminply  34524  zarcls0  34604  zarcls1  34605  zarclsiin  34607  zarclsint  34608  zarclssn  34609  qqhvval  34719  esummulc1  34817  esumcvg  34822  ofcval  34835  sigagenval  34877  measinb  34958  omsfval  35030  omssubadd  35036  sitgfval  35077  eulerpartlemsv1  35092  eulerpartlems  35096  fibp1  35137  totprobd  35162  probmeasb  35166  dstrvprob  35208  dstfrvinc  35213  dstfrvclim1  35214  ballotlemfval  35226  ballotlemsv  35246  gsumnunsn  35277  signsply0  35284  signstfval  35297  fdvneggt  35333  fdvnegge  35335  itgexpif  35339  breprexplema  35363  vtsval  35370  logdivsqrle  35383  hgt750lemg  35387  afsval  35407  lpadval  35412  cvmliftlem9  36259  goel  36313  satf0suc  36342  sat1el2xp  36345  fmlafv  36346  fmla  36347  fmlasuc0  36350  ex-sategoelel  36387  ex-sategoelelomsuc  36392  mvrsval  36471  mrsubfval  36474  mrsubval  36475  msubfval  36490  msubval  36491  msrval  36504  fwddifval  37135  fwddifnval  37136  knoppcnlem1  37567  knoppcnlem4  37570  knoppcnlem6  37572  knoppcnlem7  37573  bj-imdirval2  38365  bj-iminvval2  38376  bj-fvmptunsn2  38440  bj-endval  38497  poimirlem1  38800  poimirlem2  38801  poimirlem5  38804  poimirlem6  38805  poimirlem7  38806  poimirlem10  38809  poimirlem11  38810  poimirlem12  38811  poimirlem19  38818  poimirlem22  38821  mblfinlem2  38837  areacirc  38892  tendopl2  42093  tendoi2  42111  erngplus2  42120  erngplus2-rN  42128  hlhilset  43250  rhmzrhval  43281  lcmineqlem12  43349  aks4d1p9  43397  primrootscoprbij  43411  aks6d1c1p3  43419  aks6d1c1p5  43421  aks6d1c1  43425  hashscontpow  43431  aks6d1c3  43432  aks6d1c4  43433  aks6d1c2lem4  43436  aks6d1c2  43439  aks6d1c5lem3  43446  deg1gprod  43449  sticksstones2  43456  sticksstones3  43457  sticksstones6  43460  sticksstones7  43461  sticksstones8  43462  sticksstones10  43464  sticksstones12a  43466  sticksstones12  43467  sticksstones17  43472  sticksstones18  43473  sticksstones19  43474  aks6d1c6lem1  43479  aks6d1c6lem2  43480  aks6d1c6lem3  43481  aks6d1c6lem4  43482  aks6d1c6isolem1  43483  aks6d1c6isolem2  43484  aks6d1c6isolem3  43485  aks6d1c6lem5  43486  aks6d1c7lem1  43489  aks5lem2  43496  aks5lem3a  43498  unitscyglem1  43504  rfovfvd  45257  rfovfvfvd  45258  rfovcnvf1od  45259  rfovcnvfvd  45262  fsovfvd  45265  fsovfvfvd  45266  fsovcnvlem  45268  dssmapfv2d  45273  dssmapfv3d  45274  dssmapnvod  45275  clsk3nimkb  45295  dvgrat  45551  radcnvrat  45553  hashnzfzclim  45561  binomcxplemnn0  45588  binomcxplemrat  45589  binomcxplemfrat  45590  binomcxplemradcnv  45591  binomcxplemcvg  45593  binomcxplemdvsum  45594  binomcxplemnotnn0  45595  mapss2  46486  fmuldfeqlem1  46861  clim1fr1  46880  climrec  46882  climexp  46884  climneg  46889  divcnvg  46906  supcnvlimsup  47017  icccncfext  47164  cncfioobdlem  47173  fprodsubrecnncnvlem  47184  fprodaddrecnncnvlem  47186  dvsinax  47190  fperdvper  47196  dvcosax  47203  ioodvbdlimc1lem2  47209  ioodvbdlimc2lem  47211  dvnmul  47220  dvnprodlem1  47223  dvnprodlem2  47224  dvnprodlem3  47225  itgsinexp  47232  itgcoscmulx  47246  itgsincmulx  47251  itgsubsticclem  47252  itgsubsticc  47253  itgiccshift  47257  wallispilem5  47346  wallispi  47347  wallispi2lem1  47348  wallispi2lem2  47349  wallispi2  47350  stirlinglem1  47351  stirlinglem2  47352  stirlinglem3  47353  stirlinglem4  47354  stirlinglem5  47355  stirlinglem7  47357  stirlinglem8  47358  stirlinglem10  47360  stirlinglem11  47361  stirlinglem12  47362  stirlinglem13  47363  stirlinglem14  47364  stirlinglem15  47365  dirkerval2  47371  dirkercncflem2  47381  fourierdlem7  47391  fourierdlem13  47397  fourierdlem14  47398  fourierdlem16  47400  fourierdlem18  47402  fourierdlem19  47403  fourierdlem21  47405  fourierdlem22  47406  fourierdlem26  47410  fourierdlem37  47421  fourierdlem39  47423  fourierdlem41  47425  fourierdlem50  47433  fourierdlem51  47434  fourierdlem53  47436  fourierdlem62  47445  fourierdlem63  47446  fourierdlem65  47448  fourierdlem73  47456  fourierdlem74  47457  fourierdlem75  47458  fourierdlem76  47459  fourierdlem79  47462  fourierdlem81  47464  fourierdlem82  47465  fourierdlem83  47466  fourierdlem84  47467  fourierdlem88  47471  fourierdlem89  47472  fourierdlem90  47473  fourierdlem91  47474  fourierdlem92  47475  fourierdlem93  47476  fourierdlem97  47480  fourierdlem101  47484  fourierdlem103  47486  fourierdlem104  47487  fourierdlem111  47494  fourierdlem112  47495  fouriersw  47508  elaa2lem  47510  etransclem13  47524  etransclem17  47528  etransclem18  47529  etransclem21  47532  etransclem31  47542  etransclem32  47543  etransclem33  47544  etransclem35  47546  etransclem46  47557  etransclem48  47559  rrxtopnfi  47564  salgenval  47598  sge0val  47643  sge0z  47652  sge0snmpt  47660  sge0xp  47706  nnfoctbdjlem  47732  omeiunltfirp  47796  caratheodorylem1  47803  0ome  47806  ovnval2  47822  hoicvr  47825  ovncvrrp  47841  ovn0lem  47842  ovnsubaddlem1  47847  hsphoif  47853  hsphoival  47856  hoidmv1le  47871  hoidmvlelem3  47874  ovnhoilem2  47879  ovncvr2  47888  hoidifhspval2  47892  hoidifhspval3  47896  hspmbllem2  47904  smfid  48029  fsetsnf1  48389  fsetsnfo  48390  cfsetsnfsetfv  48394  cfsetsnfsetfo  48397  fvmptrab  48629  fundcmpsurinjlem3  48749  sprval  48828  prproropreud  48858  upgrimwlklem3  49264  grtri  49305  stgrfv  49318  isubgr3stgrlem5  49335  rngcvalALTV  49629  rngcidALTV  49638  rhmsubcALTVlem3  49647  ringcvalALTV  49653  funcringcsetcALTV2lem1  49654  ringcidALTV  49672  funcringcsetclem1ALTV  49677  linplyfv  49705  linply2cfv  49706  scmsuppss  49808  ply1mulgsum  49827  lindslinindsimp1  49894  lindsrng01  49905  islindeps2  49920  fdivmptfv  49982  refdivmptfv  49983  1arympt1fv  50076  itcoval0  50099  itcoval1  50100  itcoval2  50101  itcoval3  50102  itcovalsuc  50104  ackvalsuc1mpt  50115  ackvalsuc1  50116  ackval1  50118  ackval2  50119  ackval3  50120  ackval0val  50123  fvmpomptd  50308  swapf1a  50716  swapf2a  50718  swapf1  50719  swapf2  50721  tposcurf2val  50748  fuco23  50788  postcof2  50825  prcof1  50848  prcof21a  50851  mndtcid  51052  veronesev1lem  51395  veronesev2lem  51396  veronesev3lem  51397  veronesev4lem  51398  veronesev5lem  51399  veronesev6lem  51400  amgmwlem  51409