Theorem fvmptd 7036

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2108   ↦ cmpt 5249  ‘cfv 6573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-iota 6525  df-fun 6575  df-fv 6581

This theorem is referenced by:  fvmptd2  7037  fvmptdv2  7047  fvmptd4  7053  mptcnfimad  8027  fsplitfpar  8159  mpocurryvald  8311  ttukeylem3  10580  tpf1ofv0  14545  tpf1ofv1  14546  tpf1ofv2  14547  ccatval1  14625  ccatval2  14626  repswsymb  14822  relexp1g  15075  rtrclreclem1  15106  rtrclreclem4  15110  dfrtrcl2  15111  prmodvdslcmf  17094  prmgap  17106  prmgaplcm  17107  prmgapprmo  17109  prdsvscafval  17540  mrcval  17668  cidval  17735  subcid  17911  idfu2nd  17941  resf2nd  17959  fuccoval  18033  fucid  18041  homaval  18098  idaval  18125  setcid  18153  catcid  18174  estrcid  18202  funcestrcsetclem1  18209  funcsetcestrclem1  18223  prf1  18269  prf2  18271  curf1  18295  curf11  18296  curf2val  18300  hof2  18327  yonedalem4a  18345  vrmdval  18892  smndex1gbas  18937  smndex1gid  18938  smndex1n0mnd  18947  mulgnngsum  19119  pj1val  19737  dpjval  20100  c0mgm  20485  c0mhm  20486  c0snmgmhm  20488  c0snmhm  20489  zrrnghm  20562  zrinitorngc  20664  zrtermorngc  20665  zrtermoringc  20697  sraval  21197  rngqiprngimfv  21331  frlmphl  21824  opsrval  22087  selvfval  22161  selvval  22162  mhpval  22166  mhpsclcl  22174  psdfval  22185  psdval  22186  psdcoef  22187  cply1mul  22321  cply1coe0  22326  cply1coe0bi  22327  gsummoncoe1  22333  evls1sca  22348  mvmulfv  22571  mavmulfv  22573  mdetuni0  22648  mat2pmatval  22751  m2cpm  22768  cpm2mval  22777  m2cpminvid2lem  22781  decpmatid  22797  decpmatmullem  22798  pmatcollpw2lem  22804  monmatcollpw  22806  pm2mpfval  22823  mp2pm2mplem4  22836  pm2mpmhmlem2  22846  chpmatval  22858  fcfval  24062  cnextfval  24091  utopsnneiplem  24277  rrxmvallem  25457  rrxmval  25458  itgpowd  26111  taylpval  26426  lgamgulmlem2  27091  lgamcvglem  27101  logexprlim  27287  dchr1  27319  ishlg  28628  mirval  28681  mirfv  28682  ishpg  28785  lmif  28811  islmib  28813  lmodvslmhm  33033  psgnfzto1stlem  33093  tocycfv  33102  sgnsval  33154  evls1fldgencl  33680  minplyval  33698  rtelextdg2lem  33717  2sqr3minply  33738  madjusmdetlem2  33774  zarcls0  33814  zarcls1  33815  zarclsiin  33817  zarclsint  33818  zarclssn  33819  qqhvval  33929  indval  33977  indfval  33980  esummulc1  34045  esumcvg  34050  ofcval  34063  sigagenval  34104  measinb  34185  omsfval  34259  omssubadd  34265  sitgfval  34306  eulerpartlemsv1  34321  eulerpartlems  34325  fibp1  34366  totprobd  34391  probmeasb  34395  dstrvprob  34436  dstfrvinc  34441  dstfrvclim1  34442  ballotlemfval  34454  ballotlemsv  34474  gsumnunsn  34518  signsply0  34528  signstfval  34541  fdvneggt  34577  fdvnegge  34579  itgexpif  34583  breprexplema  34607  vtsval  34614  logdivsqrle  34627  hgt750lemg  34631  afsval  34648  lpadval  34653  cvmliftlem9  35261  goel  35315  satf0suc  35344  sat1el2xp  35347  fmlafv  35348  fmla  35349  fmlasuc0  35352  ex-sategoelel  35389  ex-sategoelelomsuc  35394  mvrsval  35473  mrsubfval  35476  mrsubval  35477  msubfval  35492  msubval  35493  msrval  35506  fwddifval  36126  fwddifnval  36127  knoppcnlem1  36459  knoppcnlem4  36462  knoppcnlem6  36464  knoppcnlem7  36465  bj-imdirval2  37149  bj-iminvval2  37160  bj-fvmptunsn2  37224  bj-endval  37281  poimirlem1  37581  poimirlem2  37582  poimirlem5  37585  poimirlem6  37586  poimirlem7  37587  poimirlem10  37590  poimirlem11  37591  poimirlem12  37592  poimirlem19  37599  poimirlem22  37602  mblfinlem2  37618  areacirc  37673  tendopl2  40734  tendoi2  40752  erngplus2  40761  erngplus2-rN  40769  hlhilset  41891  rhmzrhval  41926  lcmineqlem12  41997  aks4d1p9  42045  primrootscoprbij  42059  aks6d1c1p3  42067  aks6d1c1p5  42069  aks6d1c1  42073  hashscontpow  42079  aks6d1c3  42080  aks6d1c4  42081  aks6d1c2lem4  42084  aks6d1c2  42087  aks6d1c5lem3  42094  deg1gprod  42097  sticksstones2  42104  sticksstones3  42105  sticksstones6  42108  sticksstones7  42109  sticksstones8  42110  sticksstones10  42112  sticksstones12a  42114  sticksstones12  42115  sticksstones17  42120  sticksstones18  42121  sticksstones19  42122  aks6d1c6lem1  42127  aks6d1c6lem2  42128  aks6d1c6lem3  42129  aks6d1c6lem4  42130  aks6d1c6isolem1  42131  aks6d1c6isolem2  42132  aks6d1c6isolem3  42133  aks6d1c6lem5  42134  aks6d1c7lem1  42137  aks5lem2  42144  aks5lem3a  42146  unitscyglem1  42152  metakunt3  42164  metakunt4  42165  metakunt5  42166  metakunt6  42167  metakunt7  42168  metakunt8  42169  metakunt10  42171  metakunt11  42172  metakunt12  42173  metakunt20  42181  metakunt21  42182  metakunt22  42183  metakunt26  42187  metakunt27  42188  metakunt28  42189  metakunt29  42190  metakunt30  42191  metakunt32  42193  rfovfvd  43964  rfovfvfvd  43965  rfovcnvf1od  43966  rfovcnvfvd  43969  fsovfvd  43972  fsovfvfvd  43973  fsovcnvlem  43975  dssmapfv2d  43980  dssmapfv3d  43981  dssmapnvod  43982  clsk3nimkb  44002  dvgrat  44281  radcnvrat  44283  hashnzfzclim  44291  binomcxplemnn0  44318  binomcxplemrat  44319  binomcxplemfrat  44320  binomcxplemradcnv  44321  binomcxplemcvg  44323  binomcxplemdvsum  44324  binomcxplemnotnn0  44325  mapss2  45112  fmuldfeqlem1  45503  clim1fr1  45522  climrec  45524  climexp  45526  climneg  45531  divcnvg  45548  sumnnodd  45551  supcnvlimsup  45661  icccncfext  45808  cncfioobdlem  45817  fprodsubrecnncnvlem  45828  fprodaddrecnncnvlem  45830  dvsinax  45834  fperdvper  45840  dvcosax  45847  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  dvnmul  45864  dvnprodlem1  45867  dvnprodlem2  45868  dvnprodlem3  45869  itgsinexp  45876  itgcoscmulx  45890  itgsincmulx  45895  itgsubsticclem  45896  itgsubsticc  45897  itgiccshift  45901  wallispilem5  45990  wallispi  45991  wallispi2lem1  45992  wallispi2lem2  45993  wallispi2  45994  stirlinglem1  45995  stirlinglem2  45996  stirlinglem3  45997  stirlinglem4  45998  stirlinglem5  45999  stirlinglem7  46001  stirlinglem8  46002  stirlinglem10  46004  stirlinglem11  46005  stirlinglem12  46006  stirlinglem13  46007  stirlinglem14  46008  stirlinglem15  46009  dirkerval2  46015  dirkercncflem2  46025  fourierdlem7  46035  fourierdlem13  46041  fourierdlem14  46042  fourierdlem16  46044  fourierdlem18  46046  fourierdlem19  46047  fourierdlem21  46049  fourierdlem22  46050  fourierdlem26  46054  fourierdlem37  46065  fourierdlem39  46067  fourierdlem41  46069  fourierdlem48  46075  fourierdlem49  46076  fourierdlem50  46077  fourierdlem51  46078  fourierdlem53  46080  fourierdlem62  46089  fourierdlem63  46090  fourierdlem65  46092  fourierdlem73  46100  fourierdlem74  46101  fourierdlem75  46102  fourierdlem76  46103  fourierdlem79  46106  fourierdlem81  46108  fourierdlem82  46109  fourierdlem83  46110  fourierdlem84  46111  fourierdlem88  46115  fourierdlem89  46116  fourierdlem90  46117  fourierdlem91  46118  fourierdlem92  46119  fourierdlem93  46120  fourierdlem97  46124  fourierdlem101  46128  fourierdlem103  46130  fourierdlem104  46131  fourierdlem111  46138  fourierdlem112  46139  fouriersw  46152  elaa2lem  46154  etransclem13  46168  etransclem17  46172  etransclem18  46173  etransclem21  46176  etransclem31  46186  etransclem32  46187  etransclem33  46188  etransclem35  46190  etransclem46  46201  etransclem48  46203  rrxtopnfi  46208  salgenval  46242  sge0val  46287  sge0z  46296  sge0snmpt  46304  sge0xp  46350  nnfoctbdjlem  46376  omeiunltfirp  46440  caratheodorylem1  46447  0ome  46450  ovnval2  46466  hoicvr  46469  ovncvrrp  46485  ovn0lem  46486  ovnsubaddlem1  46491  hsphoif  46497  hsphoival  46500  hoidmv1le  46515  hoidmvlelem3  46518  ovnhoilem2  46523  ovncvr2  46532  hoidifhspval2  46536  hoidifhspval3  46540  hspmbllem2  46548  smfid  46673  fsetsnf1  46967  fsetsnfo  46968  cfsetsnfsetfv  46972  cfsetsnfsetfo  46975  fvmptrab  47207  fundcmpsurinjlem3  47274  sprval  47353  prproropreud  47383  grtri  47791  rngcvalALTV  47988  rngcidALTV  47997  rhmsubcALTVlem3  48006  ringcvalALTV  48012  funcringcsetcALTV2lem1  48013  ringcidALTV  48031  funcringcsetclem1ALTV  48036  scmsuppss  48097  ply1mulgsum  48119  lindslinindsimp1  48186  lindsrng01  48197  islindeps2  48212  fdivmptfv  48279  refdivmptfv  48280  1arympt1fv  48373  itcoval0  48396  itcoval1  48397  itcoval2  48398  itcoval3  48399  itcovalsuc  48401  ackvalsuc1mpt  48412  ackvalsuc1  48413  ackval1  48415  ackval2  48416  ackval3  48417  ackval0val  48420  mndtcid  48762  amgmwlem  48896