Theorem fvmptd 6999

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145   ↦ cmpt 5186  ‘cfv 6537

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-pr 5391

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 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-iota 6493  df-fun 6539  df-fv 6545

This theorem is used by:  fvmptd2  7000  fvmptdv2  7010  fvmptd4  7016  mptcnfimad  7996  fsplitfpar  8127  mpocurryvald  8280  ttukeylem3  10582  indval  12316  indfval  12320  tpf1ofv0  14634  tpf1ofv1  14635  tpf1ofv2  14636  ccatval1  14715  ccatval2  14716  repswsymb  14918  relexp1g  15172  rtrclreclem1  15203  rtrclreclem4  15207  dfrtrcl2  15208  prmodvdslcmf  17218  prmgap  17230  prmgaplcm  17231  prmgapprmo  17233  prdsvscafval  17644  mrcval  17777  cidval  17844  subcid  18015  idfu2nd  18045  resf2nd  18063  fuccoval  18134  fucid  18142  homaval  18199  idaval  18226  setcid  18254  catcid  18275  estrcid  18301  funcestrcsetclem1  18307  funcsetcestrclem1  18321  prf1  18367  prf2  18369  curf1  18392  curf11  18393  curf2val  18397  hof2  18424  yonedalem4a  18442  vrmdval  19046  smndex1gbasOLD  19092  smndex1gid  19093  smndex1gidOLD  19094  smndex1n0mnd  19104  mulgnngsum  19282  pj1val  19902  dpjval  20265  c0mgm  20682  c0mhm  20683  c0snmgmhm  20685  c0snmhm  20686  zrrnghm  20781  zrinitorngc  20887  zrtermorngc  20888  zrtermoringc  20920  sraval  21443  rngqiprngimfv  21587  frlmphl  22080  opsrval  22348  selvfval  22421  mhpval  22453  mhpsclcl  22461  psdfval  22472  cply1mul  22607  cply1coe0  22612  cply1coe0bi  22613  gsummoncoe1  22619  evls1sca  22634  mvmulfv  22852  mavmulfv  22854  mdetuni0  22929  mat2pmatval  23035  m2cpm  23052  cpm2mval  23061  m2cpminvid2lem  23065  decpmatid  23081  decpmatmullem  23082  pmatcollpw2lem  23088  monmatcollpw  23090  pm2mpfval  23107  mp2pm2mplem4  23120  pm2mpmhmlem2  23130  chpmatval  23142  fcfval  24345  cnextfval  24374  utopsnneiplem  24559  rrxmvallem  25718  rrxmval  25719  itgpowd  26363  taylpval  26687  lgamgulmlem2  27350  lgamcvglem  27360  logexprlim  27545  dchr1  27577  ishlg  29061  mirval  29120  mirfv  29121  ishpg  29230  lmif  29283  islmib  29285  lmodvslmhm  33604  psgnfzto1stlem  33654  tocycfv  33663  sgnsval  33715  psrnzr  34137  0mplrim  34139  selvply1rhmlemb  34144  selvply1rhmlem2  34146  mplvrpmrhm  34172  esplyfval0  34189  esplyind  34200  evls1fldgencl  34295  minplyval  34330  rtelextdg2lem  34351  2sqr3minply  34405  cos9thpiminply  34413  zarcls0  34493  zarcls1  34494  zarclsiin  34496  zarclsint  34497  zarclssn  34498  qqhvval  34608  esummulc1  34706  esumcvg  34711  ofcval  34724  sigagenval  34766  measinb  34847  omsfval  34919  omssubadd  34925  sitgfval  34966  eulerpartlemsv1  34981  eulerpartlems  34985  fibp1  35026  totprobd  35051  probmeasb  35055  dstrvprob  35097  dstfrvinc  35102  dstfrvclim1  35103  ballotlemfval  35115  ballotlemsv  35135  gsumnunsn  35166  signsply0  35173  signstfval  35186  fdvneggt  35222  fdvnegge  35224  itgexpif  35228  breprexplema  35252  vtsval  35259  logdivsqrle  35272  hgt750lemg  35276  afsval  35296  lpadval  35301  cvmliftlem9  36037  goel  36091  satf0suc  36120  sat1el2xp  36123  fmlafv  36124  fmla  36125  fmlasuc0  36128  ex-sategoelel  36165  ex-sategoelelomsuc  36170  mvrsval  36249  mrsubfval  36252  mrsubval  36253  msubfval  36268  msubval  36269  msrval  36282  fwddifval  36907  fwddifnval  36908  knoppcnlem1  37339  knoppcnlem4  37342  knoppcnlem6  37344  knoppcnlem7  37345  bj-imdirval2  38084  bj-iminvval2  38095  bj-fvmptunsn2  38159  bj-endval  38216  poimirlem1  38519  poimirlem2  38520  poimirlem5  38523  poimirlem6  38524  poimirlem7  38525  poimirlem10  38528  poimirlem11  38529  poimirlem12  38530  poimirlem19  38537  poimirlem22  38540  mblfinlem2  38556  areacirc  38611  tendopl2  41814  tendoi2  41832  erngplus2  41841  erngplus2-rN  41849  hlhilset  42971  rhmzrhval  43002  lcmineqlem12  43070  aks4d1p9  43118  primrootscoprbij  43132  aks6d1c1p3  43140  aks6d1c1p5  43142  aks6d1c1  43146  hashscontpow  43152  aks6d1c3  43153  aks6d1c4  43154  aks6d1c2lem4  43157  aks6d1c2  43160  aks6d1c5lem3  43167  deg1gprod  43170  sticksstones2  43177  sticksstones3  43178  sticksstones6  43181  sticksstones7  43182  sticksstones8  43183  sticksstones10  43185  sticksstones12a  43187  sticksstones12  43188  sticksstones17  43193  sticksstones18  43194  sticksstones19  43195  aks6d1c6lem1  43200  aks6d1c6lem2  43201  aks6d1c6lem3  43202  aks6d1c6lem4  43203  aks6d1c6isolem1  43204  aks6d1c6isolem2  43205  aks6d1c6isolem3  43206  aks6d1c6lem5  43207  aks6d1c7lem1  43210  aks5lem2  43217  aks5lem3a  43219  unitscyglem1  43225  rfovfvd  44987  rfovfvfvd  44988  rfovcnvf1od  44989  rfovcnvfvd  44992  fsovfvd  44995  fsovfvfvd  44996  fsovcnvlem  44998  dssmapfv2d  45003  dssmapfv3d  45004  dssmapnvod  45005  clsk3nimkb  45025  dvgrat  45281  radcnvrat  45283  hashnzfzclim  45291  binomcxplemnn0  45318  binomcxplemrat  45319  binomcxplemfrat  45320  binomcxplemradcnv  45321  binomcxplemcvg  45323  binomcxplemdvsum  45324  binomcxplemnotnn0  45325  mapss2  46188  fmuldfeqlem1  46563  clim1fr1  46582  climrec  46584  climexp  46586  climneg  46591  divcnvg  46608  supcnvlimsup  46719  icccncfext  46866  cncfioobdlem  46875  fprodsubrecnncnvlem  46886  fprodaddrecnncnvlem  46888  dvsinax  46892  fperdvper  46898  dvcosax  46905  ioodvbdlimc1lem2  46911  ioodvbdlimc2lem  46913  dvnmul  46922  dvnprodlem1  46925  dvnprodlem2  46926  dvnprodlem3  46927  itgsinexp  46934  itgcoscmulx  46948  itgsincmulx  46953  itgsubsticclem  46954  itgsubsticc  46955  itgiccshift  46959  wallispilem5  47048  wallispi  47049  wallispi2lem1  47050  wallispi2lem2  47051  wallispi2  47052  stirlinglem1  47053  stirlinglem2  47054  stirlinglem3  47055  stirlinglem4  47056  stirlinglem5  47057  stirlinglem7  47059  stirlinglem8  47060  stirlinglem10  47062  stirlinglem11  47063  stirlinglem12  47064  stirlinglem13  47065  stirlinglem14  47066  stirlinglem15  47067  dirkerval2  47073  dirkercncflem2  47083  fourierdlem7  47093  fourierdlem13  47099  fourierdlem14  47100  fourierdlem16  47102  fourierdlem18  47104  fourierdlem19  47105  fourierdlem21  47107  fourierdlem22  47108  fourierdlem26  47112  fourierdlem37  47123  fourierdlem39  47125  fourierdlem41  47127  fourierdlem50  47135  fourierdlem51  47136  fourierdlem53  47138  fourierdlem62  47147  fourierdlem63  47148  fourierdlem65  47150  fourierdlem73  47158  fourierdlem74  47159  fourierdlem75  47160  fourierdlem76  47161  fourierdlem79  47164  fourierdlem81  47166  fourierdlem82  47167  fourierdlem83  47168  fourierdlem84  47169  fourierdlem88  47173  fourierdlem89  47174  fourierdlem90  47175  fourierdlem91  47176  fourierdlem92  47177  fourierdlem93  47178  fourierdlem97  47182  fourierdlem101  47186  fourierdlem103  47188  fourierdlem104  47189  fourierdlem111  47196  fourierdlem112  47197  fouriersw  47210  elaa2lem  47212  etransclem13  47226  etransclem17  47230  etransclem18  47231  etransclem21  47234  etransclem31  47244  etransclem32  47245  etransclem33  47246  etransclem35  47248  etransclem46  47259  etransclem48  47261  rrxtopnfi  47266  salgenval  47300  sge0val  47345  sge0z  47354  sge0snmpt  47362  sge0xp  47408  nnfoctbdjlem  47434  omeiunltfirp  47498  caratheodorylem1  47505  0ome  47508  ovnval2  47524  hoicvr  47527  ovncvrrp  47543  ovn0lem  47544  ovnsubaddlem1  47549  hsphoif  47555  hsphoival  47558  hoidmv1le  47573  hoidmvlelem3  47576  ovnhoilem2  47581  ovncvr2  47590  hoidifhspval2  47594  hoidifhspval3  47598  hspmbllem2  47606  smfid  47731  fsetsnf1  48091  fsetsnfo  48092  cfsetsnfsetfv  48096  cfsetsnfsetfo  48099  fvmptrab  48331  fundcmpsurinjlem3  48451  sprval  48530  prproropreud  48560  upgrimwlklem3  48966  grtri  49007  stgrfv  49020  isubgr3stgrlem5  49037  rngcvalALTV  49331  rngcidALTV  49340  rhmsubcALTVlem3  49349  ringcvalALTV  49355  funcringcsetcALTV2lem1  49356  ringcidALTV  49374  funcringcsetclem1ALTV  49379  scmsuppss  49452  ply1mulgsum  49471  lindslinindsimp1  49538  lindsrng01  49549  islindeps2  49564  fdivmptfv  49626  refdivmptfv  49627  1arympt1fv  49720  itcoval0  49743  itcoval1  49744  itcoval2  49745  itcoval3  49746  itcovalsuc  49748  ackvalsuc1mpt  49759  ackvalsuc1  49760  ackval1  49762  ackval2  49763  ackval3  49764  ackval0val  49767  swapf1a  50346  swapf2a  50348  swapf1  50349  swapf2  50351  tposcurf2val  50378  fuco23  50418  prcof1  50465  prcof21a  50468  mndtcid  50666  veronesev1lem  50942  veronesev2lem  50943  veronesev3lem  50944  veronesev4lem  50945  veronesev5lem  50946  veronesev6lem  50947  amgmwlem  50956