Theorem fvmptd3 6965

Description: Deduction version of fvmpt 6941. (Contributed by Glauco Siliprandi, 23-Oct-2021.)

Hypotheses

Ref	Expression
fvmptd3.1	⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)
fvmptd3.2	⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
fvmptd3.3	⊢ (𝜑 → 𝐴 ∈ 𝐷)
fvmptd3.4	⊢ (𝜑 → 𝐶 ∈ 𝑉)

Assertion

Ref	Expression
fvmptd3	⊢ (𝜑 → (𝐹‘𝐴) = 𝐶)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐶   𝑥,𝐷

Allowed substitution hints:   𝜑(𝑥)   𝐵(𝑥)   𝐹(𝑥)   𝑉(𝑥)

Proof of Theorem fvmptd3

Step	Hyp	Ref	Expression
1		fvmptd3.3	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐷)
2		fvmptd3.4	. 2 ⊢ (𝜑 → 𝐶 ∈ 𝑉)
3		fvmptd3.2	. . 3 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶)
4		fvmptd3.1	. . 3 ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵)
5	3, 4	fvmptg 6939	. 2 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑉) → (𝐹‘𝐴) = 𝐶)
6	1, 2, 5	syl2anc 585	1 ⊢ (𝜑 → (𝐹‘𝐴) = 𝐶)

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   ↦ cmpt 5167  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-iota 6448  df-fun 6494  df-fv 6500

This theorem is referenced by:  mptmpoopabbrd  8026  undefval  8219  tz7.44-2  8339  fsetfocdm  8801  fvdiagfn  8832  resixpfo  8877  fival  9318  cantnfp1lem1  9590  cantnfp1lem2  9591  cantnfp1lem3  9592  wemapwe  9609  rankvalb  9712  djulcl  9825  djuss  9835  1stinl  9842  2ndinl  9843  1stinr  9844  2ndinr  9845  fin23lem27  10241  isf34lem1  10285  canthp1lem2  10567  wuncval  10656  indv  12152  climrlim2  15500  summolem3  15667  prodmolem3  15889  iprodmul  15959  lcmfval  16581  iserodd  16797  mreacs  17615  isofval  17715  isofn  17733  cicfval  17755  initoval  17951  termoval  17952  zerooval  17953  pwsco1mhm  18791  pwsco2mhm  18792  vrmdfval  18815  ghmqusnsglem1  19246  ghmquskerlem1  19249  galactghm  19370  symgfixfolem1  19404  pmtrval  19417  pmtrfv  19418  pmtrdifwrdellem3  19449  gsummhm2  19905  gsummpt1n0  19931  dprdfid  19985  rgspnval  20580  lspval  20961  uvcval  21775  aspval  21862  evlslem3  22068  evlsvvval  22081  psdmplcl  22138  psdadd  22139  psdmul  22142  psdmvr  22145  coe1tmfv1  22249  coe1tmfv2  22250  evls1maprhm  22351  evls1maplmhm  22352  rhmmpl  22358  rhmply1vr1  22362  rhmply1vsca  22363  mat1rhmval  22454  scmatrhmval  22502  marepvval  22542  mply1topmatval  22779  mp2pm2mplem1  22781  chfacfscmulgsum  22835  chfacfpmmulgsum  22839  tgval  22930  ntrval  23011  clsval  23012  opncldf2  23060  neival  23077  lpval  23114  1stcfb  23420  cnmpt11  23638  cnmpt21  23646  cnmptkp  23655  cnmptk1p  23660  ustval  24178  iunmbl  25530  cnmptlimc  25867  limccnp  25868  limcco  25870  coe1termlem  26233  coe1term  26234  ulmval  26358  pserulm  26400  efgh  26518  rlimcnp  26942  xrlimcnp  26945  dchrelbasd  27216  gausslemma2dlem4  27346  2lgslem1b  27369  madeval  27838  abssval  28245  tgjustr  28556  mirval  28737  midf  28858  ismidb  28860  lmif  28867  islmib  28869  wksfval  29693  crctcshwlkn0lem2  29894  crctcshwlkn0lem3  29895  wwlks  29918  wlkiswwlks2lem2  29953  wlkswwlksf1o  29962  clwwlk  30068  clwlkclwwlkf1  30095  numclwlk2lem2fv  30463  spanval  31419  fsuppcurry1  32812  fsuppcurry2  32813  mndlactf1  33101  mndlactfo  33102  mndractf1  33103  mndractfo  33104  mndlactf1o  33105  mndractf1o  33106  gsummulsubdishift1s  33146  gsummulsubdishift2s  33147  gsumwrd2dccat  33154  fzto1stfv1  33177  tocycval  33184  fxpsubm  33248  fxpsubg  33249  fxpsubrg  33250  fxpsdrg  33251  elrgspnlem1  33318  elrgspnlem2  33319  elrgspnsubrunlem2  33324  rlocf1  33349  qusrn  33484  elrspunidl  33503  elrspunsn  33504  prmidlval  33512  rprmval  33591  zringfrac  33629  ply1gsumz  33674  r1plmhm  33685  extvfvcl  33695  mplvrpmrhm  33706  psrmonmul2  33710  psrmonprod  33711  esplyfvaln  33733  vietadeg1  33737  ply1degltdimlem  33782  lactlmhm  33794  evls1fldgencl  33830  fldextrspunlsplem  33833  fldextrspunlsp  33834  ply1annidllem  33861  algextdeglem7  33883  rhmpreimacnlem  34044  esumcvg  34246  omsval  34453  eulerpartlemgvv  34536  cndprobval  34593  reprval  34770  hgt750lemb  34816  fineqvnttrclselem2  35282  fineqvnttrclselem3  35283  fineqvnttrclse  35284  satfvsuc  35559  sat1el2xp  35577  fmlasuc0  35582  climlec3  35932  fwddifval  36360  knoppcnlem1  36769  knoppcnlem9  36777  unbdqndv2lem2  36786  knoppndvlem4  36791  knoppndvlem6  36793  bj-diagval  37504  bj-endval  37645  heiborlem4  38149  heiborlem6  38151  pclvalN  40350  frlmsnic  42999  rhmpsr  43009  mplmapghm  43011  evlsbagval  43016  evlsmaprhm  43020  evlsevl  43021  selvvvval  43032  evlselv  43034  mhphflem  43043  prjspnfv01  43071  prjspner01  43072  prjspner1  43073  rabdiophlem2  43248  fphpdo  43263  monotoddzz  43389  dnnumch3lem  43492  pwssplit4  43535  hbtlem1  43569  eliunov2  44124  fvmptiunrelexplb0d  44129  fvmptiunrelexplb1d  44131  dssmapfvd  44462  wessf1ornlem  45633  projf1o  45644  fmuldfeq  46031  clim1fr1  46049  mullimcf  46071  sumnnodd  46078  expfac  46103  fnlimfv  46109  fnlimfvre2  46123  fnlimabslt  46125  limsuplt2  46199  liminfval  46205  limsupge  46207  cncfshift  46320  cncfiooicclem1  46339  fprodsubrecnncnvlem  46353  fprodaddrecnncnvlem  46355  ioodvbdlimc1lem1  46377  ioodvbdlimc1lem2  46378  dvnmul  46389  dvnprodlem1  46392  dvnprodlem2  46393  dvnprodlem3  46394  itgsinexp  46401  stoweidlem7  46453  stoweidlem17  46463  stoweidlem26  46472  stoweidlem30  46476  stoweidlem31  46477  stoweidlem32  46478  stoweidlem34  46480  wallispilem4  46514  wallispi  46516  stirlinglem3  46522  stirlinglem5  46524  stirlinglem7  46526  stirlinglem10  46529  dirkercncflem2  46550  etransclem1  46681  etransclem12  46692  etransclem27  46707  etransclem46  46726  etransclem48  46728  sge0snmptf  46883  nnfoctbdjlem  46901  psmeasurelem  46916  psmeasure  46917  meaiuninclem  46926  meaiininclem  46932  carageniuncllem1  46967  carageniuncllem2  46968  caratheodorylem1  46972  0ome  46975  vonval  46986  ovnval  46987  ovnval2b  46998  hoiprodcl2  47001  ovnlecvr  47004  ovncvrrp  47010  ovnsubaddlem1  47016  hsphoif  47022  hoidmvval  47023  hsphoival  47025  ovnhoilem1  47047  hoidifhspval  47054  hspval  47055  ovncvr2  47057  hspmbllem2  47073  ovnsubadd2lem  47091  vonioolem2  47127  vonicclem2  47130  issmflem  47173  smflimsuplem1  47266  smflimsuplem5  47270  smflimsuplem7  47272  fvmptrabdm  47753  sprsymrelfv  47966  prproropf1olem4  47978  fmtno  48004  prmdvdsfmtnof1  48062  ppivalnn  48107  upwlksfval  48623  uspgrsprfv  48633  assintopval  48693  lincop  48896  linc1  48913  lincext3  48944  el0ldep  48954  lincresunit2  48966  lincresunit3lem1  48967  blenval  49059  digfval  49085  itcoval  49149  ackval0012  49177  ackval1012  49178  ackval2012  49179  ackval3012  49180  lines  49219  spheres  49234  invfn  49517  fucoid  49835