Theorem fvmptd3 7014

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145   ↦ cmpt 5190  ‘cfv 6537

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-pr 5402

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-iota 6493  df-fun 6539  df-fv 6545

This theorem is used by:  mptmpoopabbrd  8084  undefval  8279  tz7.44-2  8400  fsetfocdm  8866  fvdiagfn  8902  resixpfo  8947  fival  9386  cantnfp1lem1  9661  cantnfp1lem2  9662  cantnfp1lem3  9663  wemapwe  9680  rankvalb  9783  djulcl  9919  djuss  9929  1stinl  9936  2ndinl  9937  1stinr  9938  2ndinr  9939  fin23lem27  10334  isf34lem1  10378  canthp1lem2  10666  wuncval  10755  indv  12248  climrlim2  15638  summolem3  15804  prodmolem3  16026  iprodmul  16096  lcmfval  16717  iserodd  16933  mreacs  17752  isofval  17852  isofn  17870  cicfval  17892  initoval  18088  termoval  18089  zerooval  18090  pwsco1mhm  18947  pwsco2mhm  18948  vrmdfval  18971  ghmqusnsglem1  19413  ghmquskerlem1  19416  galactghm  19537  symgfixfolem1  19571  pmtrval  19584  pmtrfv  19585  pmtrdifwrdellem3  19616  gsummhm2  20072  gsummpt1n0  20098  dprdfid  20152  rgspnval  20780  lspval  21165  prmidlval  21531  uvcval  22004  aspval  22093  evlslem3  22302  evlsvvval  22315  mplmapghm  22344  evlsmaprhm  22353  evlsevl  22354  selvvvval  22364  psdmplcl  22396  psdadd  22397  psdmul  22400  psdmvr  22403  coe1tmfv1  22506  coe1tmfv2  22507  evls1maprhm  22607  evls1maplmhm  22608  rhmmpl  22611  rhmply1vr1  22615  rhmply1vsca  22616  mat1rhmval  22707  scmatrhmval  22755  marepvval  22795  mply1topmatval  23035  mp2pm2mplem1  23037  chfacfscmulgsum  23091  chfacfpmmulgsum  23095  tgval  23186  ntrval  23267  clsval  23268  opncldf2  23316  neival  23333  lpval  23370  1stcfb  23676  cnmpt11  23895  cnmpt21  23903  cnmptkp  23912  cnmptk1p  23917  ustval  24435  iunmbl  25787  cnmptlimc  26124  limccnp  26125  limcco  26127  coe1termlem  26491  coe1term  26492  ulmval  26623  pserulm  26665  efgh  26786  rlimcnp  27210  xrlimcnp  27213  dchrelbasd  27483  gausslemma2dlem4  27613  2lgslem1b  27636  madeval  28105  abssval  28512  tgjustr  28823  mirval  29014  tgplnfn  29140  plngval  29142  isplng  29143  midf  29168  ismidb  29170  lmif  29177  islmib  29179  cgrabasimass  29265  angmgmval  29281  brprlng  29303  wksfval  30077  crctcshwlkn0lem2  30287  crctcshwlkn0lem3  30288  wwlks  30311  wlkiswwlks2lem2  30346  wlkswwlksf1o  30355  clwwlk  30461  clwlkclwwlkf1  30488  numclwlk2lem2fv  30866  spanval  31822  fsuppcurry1  33203  fsuppcurry2  33204  mndlactf1  33474  mndlactfo  33475  mndractf1  33476  mndractfo  33477  mndlactf1o  33478  mndractf1o  33479  gsummulsubdishift1s  33518  gsummulsubdishift2s  33519  gsumwrd2dccat  33526  fzto1stfv1  33549  tocycval  33556  fxpsubm  33620  fxpsubg  33621  fxpsubrg  33622  fxpsdrg  33623  elrgspnlem1  33690  elrgspnlem2  33691  elrgspnsubrunlem2  33696  rlocf1  33722  qusrn  33846  elrspunidl  33864  elrspunsn  33865  rprmval  33934  zringfrac  33972  ply1gsumz  34017  r1plmhm  34027  0mplrim  34032  selvply1rhmlema  34036  selvply1rhmlemb  34037  selvply1rhmlem3  34040  selvply1rhmlem5  34042  extvfvcl  34054  mplvrpmrhm  34065  psrmonmul2  34069  psrmonprod  34070  esplyfvaln  34092  vietadeg1  34096  ply1degltdimlem  34140  lactlmhm  34152  evls1fldgencl  34188  fldextrspunlsplem  34191  fldextrspunlsp  34192  ply1annidllem  34219  algextdeglem7  34241  rhmpreimacnlem  34402  esumcvg  34604  omsval  34812  eulerpartlemgvv  34895  cndprobval  34952  reprval  35126  hgt750lemb  35172  fineqvnttrclselem2  35656  fineqvnttrclselem3  35657  fineqvnttrclse  35658  satfvsuc  35948  sat1el2xp  35966  fmlasuc0  35971  climlec3  36321  fwddifval  36750  knoppcnlem1  37198  knoppcnlem9  37206  unbdqndv2lem2  37215  knoppndvlem4  37220  knoppndvlem6  37222  bj-diagval  37934  bj-endval  38075  heiborlem4  38572  heiborlem6  38574  pclvalN  40771  frlmsnic  43430  rhmpsr  43437  evlsbagval  43440  evlselv  43443  mhphflem  43450  prjspnfv01  43478  prjspner01  43479  prjspner1  43480  rabdiophlem2  43651  fphpdo  43666  monotoddzz  43792  dnnumch3lem  43895  pwssplit4  43938  hbtlem1  43972  eliunov2  44527  fvmptiunrelexplb0d  44532  fvmptiunrelexplb1d  44534  dssmapfvd  44865  wessf1ornlem  46025  projf1o  46036  fmuldfeq  46421  clim1fr1  46439  mullimcf  46461  sumnnodd  46468  expfac  46493  fnlimfv  46499  fnlimfvre2  46513  fnlimabslt  46515  limsuplt2  46589  liminfval  46595  limsupge  46597  cncfshift  46710  cncfiooicclem1  46729  fprodsubrecnncnvlem  46743  fprodaddrecnncnvlem  46745  ioodvbdlimc1lem1  46767  ioodvbdlimc1lem2  46768  dvnmul  46779  dvnprodlem1  46782  dvnprodlem2  46783  dvnprodlem3  46784  itgsinexp  46791  stoweidlem7  46843  stoweidlem17  46853  stoweidlem26  46862  stoweidlem30  46866  stoweidlem31  46867  stoweidlem32  46868  stoweidlem34  46870  wallispilem4  46904  wallispi  46906  stirlinglem3  46912  stirlinglem5  46914  stirlinglem7  46916  stirlinglem10  46919  dirkercncflem2  46940  fourierdlem48  46990  fourierdlem49  46991  etransclem1  47071  etransclem12  47082  etransclem27  47097  etransclem46  47116  etransclem48  47118  sge0snmptf  47273  nnfoctbdjlem  47291  psmeasurelem  47306  psmeasure  47307  meaiuninclem  47316  meaiininclem  47322  carageniuncllem1  47357  carageniuncllem2  47358  caratheodorylem1  47362  0ome  47365  vonval  47376  ovnval  47377  ovnval2b  47388  hoiprodcl2  47391  ovnlecvr  47394  ovncvrrp  47400  ovnsubaddlem1  47406  hsphoif  47412  hoidmvval  47413  hsphoival  47415  ovnhoilem1  47437  hoidifhspval  47444  hspval  47445  ovncvr2  47447  hspmbllem2  47463  ovnsubadd2lem  47481  vonioolem2  47517  vonicclem2  47520  issmflem  47563  smflimsuplem1  47656  smflimsuplem5  47660  smflimsuplem7  47662  tmachlem-tpitem  47776  fvmptrabdm  48189  sprsymrelfv  48402  prproropf1olem4  48414  fmtno  48440  prmdvdsfmtnof1  48498  ppivalnn  48543  upwlksfval  49059  uspgrsprfv  49069  assintopval  49128  lincop  49346  linc1  49363  lincext3  49394  el0ldep  49404  lincresunit2  49416  lincresunit3lem1  49417  blenval  49509  digfval  49535  itcoval  49599  ackval0012  49627  ackval1012  49628  ackval2012  49629  ackval3012  49630  lines  49669  spheres  49684  invfn  49964  fucoid  50282  crosspdot0lem  50804  crosspaltd  50807  crossp3d  50808  veroquadgsumlem  50824  veroquadmodzerod  50825