Theorem fvmptd3 7018

Description: Deduction version of fvmpt 6994. (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 6992	. 2 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑉) → (𝐹‘𝐴) = 𝐶)
6	1, 2, 5	syl2anc 596	1 ⊢ (𝜑 → (𝐹‘𝐴) = 𝐶)

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144   ↦ cmpt 5185  ‘cfv 6539

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-iota 6494  df-fun 6541  df-fv 6547

This theorem is used by:  mptmpoopabbrd  8095  undefval  8298  tz7.44-2  8419  fsetfocdm  8887  fvdiagfn  8923  resixpfo  8968  fival  9408  cantnfp1lem1  9683  cantnfp1lem2  9684  cantnfp1lem3  9685  wemapwe  9702  rankvalb  9809  djulcl  9995  djuss  10005  1stinl  10012  2ndinl  10013  1stinr  10014  2ndinr  10015  fin23lem27  10410  isf34lem1  10454  canthp1lem2  10742  wuncval  10831  indv  12326  climrlim2  15720  summolem3  15886  prodmolem3  16106  iprodmul  16176  lcmfval  16802  iserodd  17019  mreacs  17838  isofval  17938  isofn  17956  cicfval  17978  initoval  18174  termoval  18175  zerooval  18176  pwsco1mhm  19034  pwsco2mhm  19035  vrmdfval  19058  ghmqusnsglem1  19500  ghmquskerlem1  19503  galactghm  19624  symgfixfolem1  19658  pmtrval  19671  pmtrfv  19672  pmtrdifwrdellem3  19703  gsummhm2  20159  gsummpt1n0  20185  dprdfid  20239  rgspnval  20870  lspval  21256  prmidlval  21624  uvcval  22097  aspval  22186  evlslem3  22395  evlsvvval  22408  mplmapghm  22437  evlsmaprhm  22446  evlsevl  22447  selvvvval  22457  psdmplcl  22489  psdadd  22490  psdmul  22493  psdmvr  22496  coe1tmfv1  22599  coe1tmfv2  22600  evls1maprhm  22700  evls1maplmhm  22701  rhmmpl  22704  rhmply1vr1  22708  rhmply1vsca  22709  mat1rhmval  22800  scmatrhmval  22848  marepvval  22888  mply1topmatval  23128  mp2pm2mplem1  23130  chfacfscmulgsum  23184  chfacfpmmulgsum  23188  tgval  23279  ntrval  23360  clsval  23361  opncldf2  23409  neival  23426  lpval  23463  1stcfb  23769  cnmpt11  23988  cnmpt21  23996  cnmptkp  24005  cnmptk1p  24010  ustval  24528  iunmbl  25880  cnmptlimc  26216  limccnp  26217  limcco  26219  coe1termlem  26583  coe1term  26584  ulmval  26713  pserulm  26755  efgh  26875  rlimcnp  27299  xrlimcnp  27302  dchrelbasd  27572  gausslemma2dlem4  27702  2lgslem1b  27725  madeval  28224  abssval  28631  tgjustr  28942  mirval  29133  tgplnfn  29259  plngval  29261  isplng  29262  midf  29287  ismidb  29289  lmif  29296  islmib  29298  cgrabasimass  29384  angmgmval  29400  brprlng  29422  wksfval  30196  crctcshwlkn0lem2  30406  crctcshwlkn0lem3  30407  wwlks  30430  wlkiswwlks2lem2  30465  wlkswwlksf1o  30474  clwwlk  30580  clwlkclwwlkf1  30607  numclwlk2lem2fv  30985  spanval  31941  fsuppcurry1  33363  fsuppcurry2  33364  mndlactf1  33634  mndlactfo  33635  mndractf1  33636  mndractfo  33637  mndlactf1o  33638  mndractf1o  33639  gsummulsubdishift1s  33678  gsummulsubdishift2s  33679  gsumwrd2dccat  33686  fzto1stfv1  33709  tocycval  33716  fxpsubm  33780  fxpsubg  33781  fxpsubrg  33782  fxpsdrg  33783  elrgspnlem1  33850  elrgspnlem2  33851  elrgspnsubrunlem2  33856  rlocf1  33882  qusrn  34007  elrspunidl  34025  elrspunsn  34026  rprmval  34095  zringfrac  34133  ply1gsumz  34178  r1plmhm  34188  0mplrim  34193  selvply1rhmlema  34197  selvply1rhmlemb  34198  selvply1rhmlem3  34201  selvply1rhmlem5  34203  extvfvcl  34215  mplvrpmrhm  34226  psrmonmul2  34230  psrmonprod  34231  esplyfvaln  34253  vietadeg1  34257  ply1degltdimlem  34301  lactlmhm  34313  evls1fldgencl  34349  fldextrspunlsplem  34352  fldextrspunlsp  34353  ply1annidllem  34380  algextdeglem7  34402  rhmpreimacnlem  34563  esumcvg  34765  omsval  34972  eulerpartlemgvv  35055  cndprobval  35112  reprval  35286  hgt750lemb  35332  fineqvnttrclselem2  35847  fineqvnttrclselem3  35848  fineqvnttrclse  35849  satfvsuc  36213  sat1el2xp  36231  fmlasuc0  36236  climlec3  36592  fwddifval  37020  knoppcnlem1  37452  knoppcnlem9  37460  unbdqndv2lem2  37469  knoppndvlem4  37474  knoppndvlem6  37476  bj-diagval  38189  bj-endval  38330  heiborlem4  38842  heiborlem6  38844  pclvalN  41041  frlmsnic  43698  rhmpsr  43705  evlsbagval  43708  evlselv  43711  mhphflem  43718  frlmnzcoordval  43747  prjspnnormval  43753  rabdiophlem2  43903  fphpdo  43918  monotoddzz  44044  dnnumch3lem  44147  pwssplit4  44185  hbtlem1  44219  eliunov2  44773  fvmptiunrelexplb0d  44778  fvmptiunrelexplb1d  44780  dssmapfvd  45111  wessf1ornlem  46294  projf1o  46305  fmuldfeq  46689  clim1fr1  46707  mullimcf  46729  sumnnodd  46736  expfac  46761  fnlimfv  46767  fnlimfvre2  46781  fnlimabslt  46783  limsuplt2  46857  liminfval  46863  limsupge  46865  cncfshift  46978  cncfiooicclem1  46997  fprodsubrecnncnvlem  47011  fprodaddrecnncnvlem  47013  ioodvbdlimc1lem1  47035  ioodvbdlimc1lem2  47036  dvnmul  47047  dvnprodlem1  47050  dvnprodlem2  47051  dvnprodlem3  47052  itgsinexp  47059  stoweidlem7  47111  stoweidlem17  47121  stoweidlem26  47130  stoweidlem30  47134  stoweidlem31  47135  stoweidlem32  47136  stoweidlem34  47138  wallispilem4  47172  wallispi  47174  stirlinglem3  47180  stirlinglem5  47182  stirlinglem7  47184  stirlinglem10  47187  dirkercncflem2  47208  fourierdlem48  47258  fourierdlem49  47259  etransclem1  47339  etransclem12  47350  etransclem27  47365  etransclem46  47384  etransclem48  47386  sge0snmptf  47541  nnfoctbdjlem  47559  psmeasurelem  47574  psmeasure  47575  meaiuninclem  47584  meaiininclem  47590  carageniuncllem1  47625  carageniuncllem2  47626  caratheodorylem1  47630  0ome  47633  vonval  47644  ovnval  47645  ovnval2b  47656  hoiprodcl2  47659  ovnlecvr  47662  ovncvrrp  47668  ovnsubaddlem1  47674  hsphoif  47680  hoidmvval  47681  hsphoival  47683  ovnhoilem1  47705  hoidifhspval  47712  hspval  47713  ovncvr2  47715  hspmbllem2  47731  ovnsubadd2lem  47749  vonioolem2  47785  vonicclem2  47788  issmflem  47831  smflimsuplem1  47924  smflimsuplem5  47928  smflimsuplem7  47930  tmachlem-tpitem  48044  fvmptrabdm  48457  sprsymrelfv  48670  prproropf1olem4  48682  fmtno  48708  prmdvdsfmtnof1  48766  ppivalnn  48811  upwlksfval  49327  uspgrsprfv  49337  assintopval  49396  lincop  49614  linc1  49631  lincext3  49662  el0ldep  49672  lincresunit2  49684  lincresunit3lem1  49685  blenval  49777  digfval  49803  itcoval  49867  ackval0012  49895  ackval1012  49896  ackval2012  49897  ackval3012  49898  lines  49938  spheres  49952  invfn  50238  fucoid  50564  crosspdot0lem  51132  crosspaltd  51135  crossp3d  51136  veroquadgsumlem  51152  veroquadmodzerod  51153