Theorem fvmptd 6950

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119   ↦ cmpt 5160  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-iota 6448  df-fun 6494  df-fv 6500

This theorem is referenced by:  fvmptd2  6951  fvmptdv2  6961  fvmptd4  6967  mptcnfimad  7935  fsplitfpar  8064  mpocurryvald  8217  ttukeylem3  10431  indval  12160  indfval  12164  tpf1ofv0  14456  tpf1ofv1  14457  tpf1ofv2  14458  ccatval1  14537  ccatval2  14538  repswsymb  14734  relexp1g  14986  rtrclreclem1  15017  rtrclreclem4  15021  dfrtrcl2  15022  prmodvdslcmf  17016  prmgap  17028  prmgaplcm  17029  prmgapprmo  17031  prdsvscafval  17441  mrcval  17574  cidval  17641  subcid  17812  idfu2nd  17842  resf2nd  17860  fuccoval  17931  fucid  17939  homaval  17996  idaval  18023  setcid  18051  catcid  18072  estrcid  18098  funcestrcsetclem1  18104  funcsetcestrclem1  18118  prf1  18164  prf2  18166  curf1  18189  curf11  18190  curf2val  18194  hof2  18221  yonedalem4a  18239  vrmdval  18823  smndex1gbasOLD  18869  smndex1gid  18870  smndex1gidOLD  18871  smndex1n0mnd  18881  mulgnngsum  19053  pj1val  19668  dpjval  20031  c0mgm  20437  c0mhm  20438  c0snmgmhm  20440  c0snmhm  20441  zrrnghm  20515  zrinitorngc  20621  zrtermorngc  20622  zrtermoringc  20654  sraval  21172  rngqiprngimfv  21298  frlmphl  21763  opsrval  22029  selvfval  22102  mhpval  22134  mhpsclcl  22142  psdfval  22153  cply1mul  22289  cply1coe0  22294  cply1coe0bi  22295  gsummoncoe1  22301  evls1sca  22316  mvmulfv  22534  mavmulfv  22536  mdetuni0  22611  mat2pmatval  22714  m2cpm  22731  cpm2mval  22740  m2cpminvid2lem  22744  decpmatid  22760  decpmatmullem  22761  pmatcollpw2lem  22767  monmatcollpw  22769  pm2mpfval  22786  mp2pm2mplem4  22799  pm2mpmhmlem2  22809  chpmatval  22821  fcfval  24023  cnextfval  24052  utopsnneiplem  24237  rrxmvallem  25396  rrxmval  25397  itgpowd  26042  taylpval  26357  lgamgulmlem2  27018  lgamcvglem  27028  logexprlim  27213  dchr1  27245  ishlg  28695  mirval  28748  mirfv  28749  ishpg  28852  lmif  28878  islmib  28880  lmodvslmhm  33138  psgnfzto1stlem  33188  tocycfv  33197  sgnsval  33249  psrnzr  33703  0mplrim  33705  selvply1rhmlemb  33710  selvply1rhmlem2  33712  mplvrpmrhm  33738  esplyfval0  33755  esplyind  33766  evls1fldgencl  33861  minplyval  33896  rtelextdg2lem  33917  2sqr3minply  33971  cos9thpiminply  33979  zarcls0  34059  zarcls1  34060  zarclsiin  34062  zarclsint  34063  zarclssn  34064  qqhvval  34174  esummulc1  34272  esumcvg  34277  ofcval  34290  sigagenval  34331  measinb  34412  omsfval  34485  omssubadd  34491  sitgfval  34532  eulerpartlemsv1  34547  eulerpartlems  34551  fibp1  34592  totprobd  34617  probmeasb  34621  dstrvprob  34663  dstfrvinc  34668  dstfrvclim1  34669  ballotlemfval  34681  ballotlemsv  34701  gsumnunsn  34732  signsply0  34742  signstfval  34755  fdvneggt  34791  fdvnegge  34793  itgexpif  34797  breprexplema  34821  vtsval  34828  logdivsqrle  34841  hgt750lemg  34845  afsval  34862  lpadval  34867  cvmliftlem9  35528  goel  35582  satf0suc  35611  sat1el2xp  35614  fmlafv  35615  fmla  35616  fmlasuc0  35619  ex-sategoelel  35656  ex-sategoelelomsuc  35661  mvrsval  35740  mrsubfval  35743  mrsubval  35744  msubfval  35759  msubval  35760  msrval  35773  fwddifval  36397  fwddifnval  36398  knoppcnlem1  36806  knoppcnlem4  36809  knoppcnlem6  36811  knoppcnlem7  36812  bj-imdirval2  37550  bj-iminvval2  37561  bj-fvmptunsn2  37625  bj-endval  37682  poimirlem1  37995  poimirlem2  37996  poimirlem5  37999  poimirlem6  38000  poimirlem7  38001  poimirlem10  38004  poimirlem11  38005  poimirlem12  38006  poimirlem19  38013  poimirlem22  38016  mblfinlem2  38032  areacirc  38087  tendopl2  41276  tendoi2  41294  erngplus2  41303  erngplus2-rN  41311  hlhilset  42433  rhmzrhval  42464  lcmineqlem12  42532  aks4d1p9  42580  primrootscoprbij  42594  aks6d1c1p3  42602  aks6d1c1p5  42604  aks6d1c1  42608  hashscontpow  42614  aks6d1c3  42615  aks6d1c4  42616  aks6d1c2lem4  42619  aks6d1c2  42622  aks6d1c5lem3  42629  deg1gprod  42632  sticksstones2  42639  sticksstones3  42640  sticksstones6  42643  sticksstones7  42644  sticksstones8  42645  sticksstones10  42647  sticksstones12a  42649  sticksstones12  42650  sticksstones17  42655  sticksstones18  42656  sticksstones19  42657  aks6d1c6lem1  42662  aks6d1c6lem2  42663  aks6d1c6lem3  42664  aks6d1c6lem4  42665  aks6d1c6isolem1  42666  aks6d1c6isolem2  42667  aks6d1c6isolem3  42668  aks6d1c6lem5  42669  aks6d1c7lem1  42672  aks5lem2  42679  aks5lem3a  42681  unitscyglem1  42687  rfovfvd  44453  rfovfvfvd  44454  rfovcnvf1od  44455  rfovcnvfvd  44458  fsovfvd  44461  fsovfvfvd  44462  fsovcnvlem  44464  dssmapfv2d  44469  dssmapfv3d  44470  dssmapnvod  44471  clsk3nimkb  44491  dvgrat  44763  radcnvrat  44765  hashnzfzclim  44773  binomcxplemnn0  44800  binomcxplemrat  44801  binomcxplemfrat  44802  binomcxplemradcnv  44803  binomcxplemcvg  44805  binomcxplemdvsum  44806  binomcxplemnotnn0  44807  mapss2  45658  fmuldfeqlem1  46034  clim1fr1  46053  climrec  46055  climexp  46057  climneg  46062  divcnvg  46079  sumnnodd  46082  supcnvlimsup  46190  icccncfext  46337  cncfioobdlem  46346  fprodsubrecnncnvlem  46357  fprodaddrecnncnvlem  46359  dvsinax  46363  fperdvper  46369  dvcosax  46376  ioodvbdlimc1lem2  46382  ioodvbdlimc2lem  46384  dvnmul  46393  dvnprodlem1  46396  dvnprodlem2  46397  dvnprodlem3  46398  itgsinexp  46405  itgcoscmulx  46419  itgsincmulx  46424  itgsubsticclem  46425  itgsubsticc  46426  itgiccshift  46430  wallispilem5  46519  wallispi  46520  wallispi2lem1  46521  wallispi2lem2  46522  wallispi2  46523  stirlinglem1  46524  stirlinglem2  46525  stirlinglem3  46526  stirlinglem4  46527  stirlinglem5  46528  stirlinglem7  46530  stirlinglem8  46531  stirlinglem10  46533  stirlinglem11  46534  stirlinglem12  46535  stirlinglem13  46536  stirlinglem14  46537  stirlinglem15  46538  dirkerval2  46544  dirkercncflem2  46554  fourierdlem7  46564  fourierdlem13  46570  fourierdlem14  46571  fourierdlem16  46573  fourierdlem18  46575  fourierdlem19  46576  fourierdlem21  46578  fourierdlem22  46579  fourierdlem26  46583  fourierdlem37  46594  fourierdlem39  46596  fourierdlem41  46598  fourierdlem48  46604  fourierdlem49  46605  fourierdlem50  46606  fourierdlem51  46607  fourierdlem53  46609  fourierdlem62  46618  fourierdlem63  46619  fourierdlem65  46621  fourierdlem73  46629  fourierdlem74  46630  fourierdlem75  46631  fourierdlem76  46632  fourierdlem79  46635  fourierdlem81  46637  fourierdlem82  46638  fourierdlem83  46639  fourierdlem84  46640  fourierdlem88  46644  fourierdlem89  46645  fourierdlem90  46646  fourierdlem91  46647  fourierdlem92  46648  fourierdlem93  46649  fourierdlem97  46653  fourierdlem101  46657  fourierdlem103  46659  fourierdlem104  46660  fourierdlem111  46667  fourierdlem112  46668  fouriersw  46681  elaa2lem  46683  etransclem13  46697  etransclem17  46701  etransclem18  46702  etransclem21  46705  etransclem31  46715  etransclem32  46716  etransclem33  46717  etransclem35  46719  etransclem46  46730  etransclem48  46732  rrxtopnfi  46737  salgenval  46771  sge0val  46816  sge0z  46825  sge0snmpt  46833  sge0xp  46879  nnfoctbdjlem  46905  omeiunltfirp  46969  caratheodorylem1  46976  0ome  46979  ovnval2  46995  hoicvr  46998  ovncvrrp  47014  ovn0lem  47015  ovnsubaddlem1  47020  hsphoif  47026  hsphoival  47029  hoidmv1le  47044  hoidmvlelem3  47047  ovnhoilem2  47052  ovncvr2  47061  hoidifhspval2  47065  hoidifhspval3  47069  hspmbllem2  47077  smfid  47202  fsetsnf1  47522  fsetsnfo  47523  cfsetsnfsetfv  47527  cfsetsnfsetfo  47530  fvmptrab  47762  fundcmpsurinjlem3  47882  sprval  47961  prproropreud  47991  upgrimwlklem3  48397  grtri  48438  stgrfv  48451  isubgr3stgrlem5  48468  rngcvalALTV  48763  rngcidALTV  48772  rhmsubcALTVlem3  48781  ringcvalALTV  48787  funcringcsetcALTV2lem1  48788  ringcidALTV  48806  funcringcsetclem1ALTV  48811  scmsuppss  48869  ply1mulgsum  48888  lindslinindsimp1  48955  lindsrng01  48966  islindeps2  48981  fdivmptfv  49043  refdivmptfv  49044  1arympt1fv  49137  itcoval0  49160  itcoval1  49161  itcoval2  49162  itcoval3  49163  itcovalsuc  49165  ackvalsuc1mpt  49176  ackvalsuc1  49177  ackval1  49179  ackval2  49180  ackval3  49181  ackval0val  49184  swapf1a  49766  swapf2a  49768  swapf1  49769  swapf2  49771  tposcurf2val  49798  fuco23  49838  prcof1  49885  prcof21a  49888  mndtcid  50086  amgmwlem  50299