Theorem fvmptd 6975

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109   ↦ cmpt 5188  ‘cfv 6511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-iota 6464  df-fun 6513  df-fv 6519

This theorem is referenced by:  fvmptd2  6976  fvmptdv2  6986  fvmptd4  6992  mptcnfimad  7965  fsplitfpar  8097  mpocurryvald  8249  ttukeylem3  10464  tpf1ofv0  14461  tpf1ofv1  14462  tpf1ofv2  14463  ccatval1  14542  ccatval2  14543  repswsymb  14739  relexp1g  14992  rtrclreclem1  15023  rtrclreclem4  15027  dfrtrcl2  15028  prmodvdslcmf  17018  prmgap  17030  prmgaplcm  17031  prmgapprmo  17033  prdsvscafval  17443  mrcval  17571  cidval  17638  subcid  17809  idfu2nd  17839  resf2nd  17857  fuccoval  17928  fucid  17936  homaval  17993  idaval  18020  setcid  18048  catcid  18069  estrcid  18095  funcestrcsetclem1  18101  funcsetcestrclem1  18115  prf1  18161  prf2  18163  curf1  18186  curf11  18187  curf2val  18191  hof2  18218  yonedalem4a  18236  vrmdval  18784  smndex1gbas  18829  smndex1gid  18830  smndex1n0mnd  18839  mulgnngsum  19011  pj1val  19625  dpjval  19988  c0mgm  20368  c0mhm  20369  c0snmgmhm  20371  c0snmhm  20372  zrrnghm  20445  zrinitorngc  20551  zrtermorngc  20552  zrtermoringc  20584  sraval  21082  rngqiprngimfv  21208  frlmphl  21690  opsrval  21953  selvfval  22021  mhpval  22026  mhpsclcl  22034  psdfval  22045  cply1mul  22183  cply1coe0  22188  cply1coe0bi  22189  gsummoncoe1  22195  evls1sca  22210  mvmulfv  22431  mavmulfv  22433  mdetuni0  22508  mat2pmatval  22611  m2cpm  22628  cpm2mval  22637  m2cpminvid2lem  22641  decpmatid  22657  decpmatmullem  22658  pmatcollpw2lem  22664  monmatcollpw  22666  pm2mpfval  22683  mp2pm2mplem4  22696  pm2mpmhmlem2  22706  chpmatval  22718  fcfval  23920  cnextfval  23949  utopsnneiplem  24135  rrxmvallem  25304  rrxmval  25305  itgpowd  25957  taylpval  26274  lgamgulmlem2  26940  lgamcvglem  26950  logexprlim  27136  dchr1  27168  ishlg  28529  mirval  28582  mirfv  28583  ishpg  28686  lmif  28712  islmib  28714  indval  32776  indfval  32779  lmodvslmhm  32990  psgnfzto1stlem  33057  tocycfv  33066  sgnsval  33118  evls1fldgencl  33665  minplyval  33695  rtelextdg2lem  33716  2sqr3minply  33770  cos9thpiminply  33778  zarcls0  33858  zarcls1  33859  zarclsiin  33861  zarclsint  33862  zarclssn  33863  qqhvval  33973  esummulc1  34071  esumcvg  34076  ofcval  34089  sigagenval  34130  measinb  34211  omsfval  34285  omssubadd  34291  sitgfval  34332  eulerpartlemsv1  34347  eulerpartlems  34351  fibp1  34392  totprobd  34417  probmeasb  34421  dstrvprob  34463  dstfrvinc  34468  dstfrvclim1  34469  ballotlemfval  34481  ballotlemsv  34501  gsumnunsn  34532  signsply0  34542  signstfval  34555  fdvneggt  34591  fdvnegge  34593  itgexpif  34597  breprexplema  34621  vtsval  34628  logdivsqrle  34641  hgt750lemg  34645  afsval  34662  lpadval  34667  cvmliftlem9  35280  goel  35334  satf0suc  35363  sat1el2xp  35366  fmlafv  35367  fmla  35368  fmlasuc0  35371  ex-sategoelel  35408  ex-sategoelelomsuc  35413  mvrsval  35492  mrsubfval  35495  mrsubval  35496  msubfval  35511  msubval  35512  msrval  35525  fwddifval  36150  fwddifnval  36151  knoppcnlem1  36481  knoppcnlem4  36484  knoppcnlem6  36486  knoppcnlem7  36487  bj-imdirval2  37171  bj-iminvval2  37182  bj-fvmptunsn2  37246  bj-endval  37303  poimirlem1  37615  poimirlem2  37616  poimirlem5  37619  poimirlem6  37620  poimirlem7  37621  poimirlem10  37624  poimirlem11  37625  poimirlem12  37626  poimirlem19  37633  poimirlem22  37636  mblfinlem2  37652  areacirc  37707  tendopl2  40771  tendoi2  40789  erngplus2  40798  erngplus2-rN  40806  hlhilset  41928  rhmzrhval  41959  lcmineqlem12  42028  aks4d1p9  42076  primrootscoprbij  42090  aks6d1c1p3  42098  aks6d1c1p5  42100  aks6d1c1  42104  hashscontpow  42110  aks6d1c3  42111  aks6d1c4  42112  aks6d1c2lem4  42115  aks6d1c2  42118  aks6d1c5lem3  42125  deg1gprod  42128  sticksstones2  42135  sticksstones3  42136  sticksstones6  42139  sticksstones7  42140  sticksstones8  42141  sticksstones10  42143  sticksstones12a  42145  sticksstones12  42146  sticksstones17  42151  sticksstones18  42152  sticksstones19  42153  aks6d1c6lem1  42158  aks6d1c6lem2  42159  aks6d1c6lem3  42160  aks6d1c6lem4  42161  aks6d1c6isolem1  42162  aks6d1c6isolem2  42163  aks6d1c6isolem3  42164  aks6d1c6lem5  42165  aks6d1c7lem1  42168  aks5lem2  42175  aks5lem3a  42177  unitscyglem1  42183  rfovfvd  43991  rfovfvfvd  43992  rfovcnvf1od  43993  rfovcnvfvd  43996  fsovfvd  43999  fsovfvfvd  44000  fsovcnvlem  44002  dssmapfv2d  44007  dssmapfv3d  44008  dssmapnvod  44009  clsk3nimkb  44029  dvgrat  44301  radcnvrat  44303  hashnzfzclim  44311  binomcxplemnn0  44338  binomcxplemrat  44339  binomcxplemfrat  44340  binomcxplemradcnv  44341  binomcxplemcvg  44343  binomcxplemdvsum  44344  binomcxplemnotnn0  44345  mapss2  45199  fmuldfeqlem1  45580  clim1fr1  45599  climrec  45601  climexp  45603  climneg  45608  divcnvg  45625  sumnnodd  45628  supcnvlimsup  45738  icccncfext  45885  cncfioobdlem  45894  fprodsubrecnncnvlem  45905  fprodaddrecnncnvlem  45907  dvsinax  45911  fperdvper  45917  dvcosax  45924  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  dvnmul  45941  dvnprodlem1  45944  dvnprodlem2  45945  dvnprodlem3  45946  itgsinexp  45953  itgcoscmulx  45967  itgsincmulx  45972  itgsubsticclem  45973  itgsubsticc  45974  itgiccshift  45978  wallispilem5  46067  wallispi  46068  wallispi2lem1  46069  wallispi2lem2  46070  wallispi2  46071  stirlinglem1  46072  stirlinglem2  46073  stirlinglem3  46074  stirlinglem4  46075  stirlinglem5  46076  stirlinglem7  46078  stirlinglem8  46079  stirlinglem10  46081  stirlinglem11  46082  stirlinglem12  46083  stirlinglem13  46084  stirlinglem14  46085  stirlinglem15  46086  dirkerval2  46092  dirkercncflem2  46102  fourierdlem7  46112  fourierdlem13  46118  fourierdlem14  46119  fourierdlem16  46121  fourierdlem18  46123  fourierdlem19  46124  fourierdlem21  46126  fourierdlem22  46127  fourierdlem26  46131  fourierdlem37  46142  fourierdlem39  46144  fourierdlem41  46146  fourierdlem48  46152  fourierdlem49  46153  fourierdlem50  46154  fourierdlem51  46155  fourierdlem53  46157  fourierdlem62  46166  fourierdlem63  46167  fourierdlem65  46169  fourierdlem73  46177  fourierdlem74  46178  fourierdlem75  46179  fourierdlem76  46180  fourierdlem79  46183  fourierdlem81  46185  fourierdlem82  46186  fourierdlem83  46187  fourierdlem84  46188  fourierdlem88  46192  fourierdlem89  46193  fourierdlem90  46194  fourierdlem91  46195  fourierdlem92  46196  fourierdlem93  46197  fourierdlem97  46201  fourierdlem101  46205  fourierdlem103  46207  fourierdlem104  46208  fourierdlem111  46215  fourierdlem112  46216  fouriersw  46229  elaa2lem  46231  etransclem13  46245  etransclem17  46249  etransclem18  46250  etransclem21  46253  etransclem31  46263  etransclem32  46264  etransclem33  46265  etransclem35  46267  etransclem46  46278  etransclem48  46280  rrxtopnfi  46285  salgenval  46319  sge0val  46364  sge0z  46373  sge0snmpt  46381  sge0xp  46427  nnfoctbdjlem  46453  omeiunltfirp  46517  caratheodorylem1  46524  0ome  46527  ovnval2  46543  hoicvr  46546  ovncvrrp  46562  ovn0lem  46563  ovnsubaddlem1  46568  hsphoif  46574  hsphoival  46577  hoidmv1le  46592  hoidmvlelem3  46595  ovnhoilem2  46600  ovncvr2  46609  hoidifhspval2  46613  hoidifhspval3  46617  hspmbllem2  46625  smfid  46750  fsetsnf1  47053  fsetsnfo  47054  cfsetsnfsetfv  47058  cfsetsnfsetfo  47061  fvmptrab  47293  fundcmpsurinjlem3  47401  sprval  47480  prproropreud  47510  upgrimwlklem3  47899  grtri  47939  stgrfv  47952  isubgr3stgrlem5  47969  rngcvalALTV  48253  rngcidALTV  48262  rhmsubcALTVlem3  48271  ringcvalALTV  48277  funcringcsetcALTV2lem1  48278  ringcidALTV  48296  funcringcsetclem1ALTV  48301  scmsuppss  48359  ply1mulgsum  48379  lindslinindsimp1  48446  lindsrng01  48457  islindeps2  48472  fdivmptfv  48534  refdivmptfv  48535  1arympt1fv  48628  itcoval0  48651  itcoval1  48652  itcoval2  48653  itcoval3  48654  itcovalsuc  48656  ackvalsuc1mpt  48667  ackvalsuc1  48668  ackval1  48670  ackval2  48671  ackval3  48672  ackval0val  48675  swapf1a  49258  swapf2a  49260  swapf1  49261  swapf2  49263  tposcurf2val  49290  fuco23  49330  prcof1  49377  prcof21a  49380  mndtcid  49578  amgmwlem  49791