Theorem fvmptd 7022

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1536   ∈ wcel 2105   ↦ cmpt 5230  ‘cfv 6562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-iota 6515  df-fun 6564  df-fv 6570

This theorem is referenced by:  fvmptd2  7023  fvmptdv2  7033  fvmptd4  7039  mptcnfimad  8009  fsplitfpar  8141  mpocurryvald  8293  ttukeylem3  10548  tpf1ofv0  14531  tpf1ofv1  14532  tpf1ofv2  14533  ccatval1  14611  ccatval2  14612  repswsymb  14808  relexp1g  15061  rtrclreclem1  15092  rtrclreclem4  15096  dfrtrcl2  15097  prmodvdslcmf  17080  prmgap  17092  prmgaplcm  17093  prmgapprmo  17095  prdsvscafval  17526  mrcval  17654  cidval  17721  subcid  17897  idfu2nd  17927  resf2nd  17945  fuccoval  18019  fucid  18027  homaval  18084  idaval  18111  setcid  18139  catcid  18160  estrcid  18188  funcestrcsetclem1  18195  funcsetcestrclem1  18209  prf1  18255  prf2  18257  curf1  18281  curf11  18282  curf2val  18286  hof2  18313  yonedalem4a  18331  vrmdval  18882  smndex1gbas  18927  smndex1gid  18928  smndex1n0mnd  18937  mulgnngsum  19109  pj1val  19727  dpjval  20090  c0mgm  20475  c0mhm  20476  c0snmgmhm  20478  c0snmhm  20479  zrrnghm  20552  zrinitorngc  20658  zrtermorngc  20659  zrtermoringc  20691  sraval  21191  rngqiprngimfv  21325  frlmphl  21818  opsrval  22081  selvfval  22155  mhpval  22160  mhpsclcl  22168  psdfval  22179  cply1mul  22315  cply1coe0  22320  cply1coe0bi  22321  gsummoncoe1  22327  evls1sca  22342  mvmulfv  22565  mavmulfv  22567  mdetuni0  22642  mat2pmatval  22745  m2cpm  22762  cpm2mval  22771  m2cpminvid2lem  22775  decpmatid  22791  decpmatmullem  22792  pmatcollpw2lem  22798  monmatcollpw  22800  pm2mpfval  22817  mp2pm2mplem4  22830  pm2mpmhmlem2  22840  chpmatval  22852  fcfval  24056  cnextfval  24085  utopsnneiplem  24271  rrxmvallem  25451  rrxmval  25452  itgpowd  26105  taylpval  26422  lgamgulmlem2  27087  lgamcvglem  27097  logexprlim  27283  dchr1  27315  ishlg  28624  mirval  28677  mirfv  28678  ishpg  28781  lmif  28807  islmib  28809  lmodvslmhm  33035  psgnfzto1stlem  33102  tocycfv  33111  sgnsval  33163  evls1fldgencl  33694  minplyval  33712  rtelextdg2lem  33731  2sqr3minply  33752  zarcls0  33828  zarcls1  33829  zarclsiin  33831  zarclsint  33832  zarclssn  33833  qqhvval  33945  indval  33993  indfval  33996  esummulc1  34061  esumcvg  34066  ofcval  34079  sigagenval  34120  measinb  34201  omsfval  34275  omssubadd  34281  sitgfval  34322  eulerpartlemsv1  34337  eulerpartlems  34341  fibp1  34382  totprobd  34407  probmeasb  34411  dstrvprob  34452  dstfrvinc  34457  dstfrvclim1  34458  ballotlemfval  34470  ballotlemsv  34490  gsumnunsn  34534  signsply0  34544  signstfval  34557  fdvneggt  34593  fdvnegge  34595  itgexpif  34599  breprexplema  34623  vtsval  34630  logdivsqrle  34643  hgt750lemg  34647  afsval  34664  lpadval  34669  cvmliftlem9  35277  goel  35331  satf0suc  35360  sat1el2xp  35363  fmlafv  35364  fmla  35365  fmlasuc0  35368  ex-sategoelel  35405  ex-sategoelelomsuc  35410  mvrsval  35489  mrsubfval  35492  mrsubval  35493  msubfval  35508  msubval  35509  msrval  35522  fwddifval  36143  fwddifnval  36144  knoppcnlem1  36475  knoppcnlem4  36478  knoppcnlem6  36480  knoppcnlem7  36481  bj-imdirval2  37165  bj-iminvval2  37176  bj-fvmptunsn2  37240  bj-endval  37297  poimirlem1  37607  poimirlem2  37608  poimirlem5  37611  poimirlem6  37612  poimirlem7  37613  poimirlem10  37616  poimirlem11  37617  poimirlem12  37618  poimirlem19  37625  poimirlem22  37628  mblfinlem2  37644  areacirc  37699  tendopl2  40759  tendoi2  40777  erngplus2  40786  erngplus2-rN  40794  hlhilset  41916  rhmzrhval  41951  lcmineqlem12  42021  aks4d1p9  42069  primrootscoprbij  42083  aks6d1c1p3  42091  aks6d1c1p5  42093  aks6d1c1  42097  hashscontpow  42103  aks6d1c3  42104  aks6d1c4  42105  aks6d1c2lem4  42108  aks6d1c2  42111  aks6d1c5lem3  42118  deg1gprod  42121  sticksstones2  42128  sticksstones3  42129  sticksstones6  42132  sticksstones7  42133  sticksstones8  42134  sticksstones10  42136  sticksstones12a  42138  sticksstones12  42139  sticksstones17  42144  sticksstones18  42145  sticksstones19  42146  aks6d1c6lem1  42151  aks6d1c6lem2  42152  aks6d1c6lem3  42153  aks6d1c6lem4  42154  aks6d1c6isolem1  42155  aks6d1c6isolem2  42156  aks6d1c6isolem3  42157  aks6d1c6lem5  42158  aks6d1c7lem1  42161  aks5lem2  42168  aks5lem3a  42170  unitscyglem1  42176  metakunt3  42188  metakunt4  42189  metakunt5  42190  metakunt6  42191  metakunt7  42192  metakunt8  42193  metakunt10  42195  metakunt11  42196  metakunt12  42197  metakunt20  42205  metakunt21  42206  metakunt22  42207  metakunt26  42211  metakunt27  42212  metakunt28  42213  metakunt29  42214  metakunt30  42215  metakunt32  42217  rfovfvd  43991  rfovfvfvd  43992  rfovcnvf1od  43993  rfovcnvfvd  43996  fsovfvd  43999  fsovfvfvd  44000  fsovcnvlem  44002  dssmapfv2d  44007  dssmapfv3d  44008  dssmapnvod  44009  clsk3nimkb  44029  dvgrat  44307  radcnvrat  44309  hashnzfzclim  44317  binomcxplemnn0  44344  binomcxplemrat  44345  binomcxplemfrat  44346  binomcxplemradcnv  44347  binomcxplemcvg  44349  binomcxplemdvsum  44350  binomcxplemnotnn0  44351  mapss2  45147  fmuldfeqlem1  45537  clim1fr1  45556  climrec  45558  climexp  45560  climneg  45565  divcnvg  45582  sumnnodd  45585  supcnvlimsup  45695  icccncfext  45842  cncfioobdlem  45851  fprodsubrecnncnvlem  45862  fprodaddrecnncnvlem  45864  dvsinax  45868  fperdvper  45874  dvcosax  45881  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  dvnmul  45898  dvnprodlem1  45901  dvnprodlem2  45902  dvnprodlem3  45903  itgsinexp  45910  itgcoscmulx  45924  itgsincmulx  45929  itgsubsticclem  45930  itgsubsticc  45931  itgiccshift  45935  wallispilem5  46024  wallispi  46025  wallispi2lem1  46026  wallispi2lem2  46027  wallispi2  46028  stirlinglem1  46029  stirlinglem2  46030  stirlinglem3  46031  stirlinglem4  46032  stirlinglem5  46033  stirlinglem7  46035  stirlinglem8  46036  stirlinglem10  46038  stirlinglem11  46039  stirlinglem12  46040  stirlinglem13  46041  stirlinglem14  46042  stirlinglem15  46043  dirkerval2  46049  dirkercncflem2  46059  fourierdlem7  46069  fourierdlem13  46075  fourierdlem14  46076  fourierdlem16  46078  fourierdlem18  46080  fourierdlem19  46081  fourierdlem21  46083  fourierdlem22  46084  fourierdlem26  46088  fourierdlem37  46099  fourierdlem39  46101  fourierdlem41  46103  fourierdlem48  46109  fourierdlem49  46110  fourierdlem50  46111  fourierdlem51  46112  fourierdlem53  46114  fourierdlem62  46123  fourierdlem63  46124  fourierdlem65  46126  fourierdlem73  46134  fourierdlem74  46135  fourierdlem75  46136  fourierdlem76  46137  fourierdlem79  46140  fourierdlem81  46142  fourierdlem82  46143  fourierdlem83  46144  fourierdlem84  46145  fourierdlem88  46149  fourierdlem89  46150  fourierdlem90  46151  fourierdlem91  46152  fourierdlem92  46153  fourierdlem93  46154  fourierdlem97  46158  fourierdlem101  46162  fourierdlem103  46164  fourierdlem104  46165  fourierdlem111  46172  fourierdlem112  46173  fouriersw  46186  elaa2lem  46188  etransclem13  46202  etransclem17  46206  etransclem18  46207  etransclem21  46210  etransclem31  46220  etransclem32  46221  etransclem33  46222  etransclem35  46224  etransclem46  46235  etransclem48  46237  rrxtopnfi  46242  salgenval  46276  sge0val  46321  sge0z  46330  sge0snmpt  46338  sge0xp  46384  nnfoctbdjlem  46410  omeiunltfirp  46474  caratheodorylem1  46481  0ome  46484  ovnval2  46500  hoicvr  46503  ovncvrrp  46519  ovn0lem  46520  ovnsubaddlem1  46525  hsphoif  46531  hsphoival  46534  hoidmv1le  46549  hoidmvlelem3  46552  ovnhoilem2  46557  ovncvr2  46566  hoidifhspval2  46570  hoidifhspval3  46574  hspmbllem2  46582  smfid  46707  fsetsnf1  47001  fsetsnfo  47002  cfsetsnfsetfv  47006  cfsetsnfsetfo  47009  fvmptrab  47241  fundcmpsurinjlem3  47324  sprval  47403  prproropreud  47433  grtri  47844  stgrfv  47855  isubgr3stgrlem5  47872  rngcvalALTV  48108  rngcidALTV  48117  rhmsubcALTVlem3  48126  ringcvalALTV  48132  funcringcsetcALTV2lem1  48133  ringcidALTV  48151  funcringcsetclem1ALTV  48156  scmsuppss  48215  ply1mulgsum  48235  lindslinindsimp1  48302  lindsrng01  48313  islindeps2  48328  fdivmptfv  48394  refdivmptfv  48395  1arympt1fv  48488  itcoval0  48511  itcoval1  48512  itcoval2  48513  itcoval3  48514  itcovalsuc  48516  ackvalsuc1mpt  48527  ackvalsuc1  48528  ackval1  48530  ackval2  48531  ackval3  48532  ackval0val  48535  mndtcid  48897  amgmwlem  49032