Theorem fvmptd3 7038

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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105   ↦ cmpt 5230  ‘cfv 6562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-iota 6515  df-fun 6564  df-fv 6570

This theorem is referenced by:  mptmpoopabbrd  8103  mptmpoopabbrdOLD  8104  mptmpoopabbrdOLDOLD  8106  undefval  8299  tz7.44-2  8445  fsetfocdm  8899  fvdiagfn  8929  resixpfo  8974  fival  9449  cantnfp1lem1  9715  cantnfp1lem2  9716  cantnfp1lem3  9717  wemapwe  9734  rankvalb  9834  djulcl  9947  djuss  9957  1stinl  9964  2ndinl  9965  1stinr  9966  2ndinr  9967  fin23lem27  10365  isf34lem1  10409  canthp1lem2  10690  wuncval  10779  climrlim2  15579  summolem3  15746  prodmolem3  15965  iprodmul  16035  lcmfval  16654  iserodd  16868  mreacs  17702  isofval  17804  isofn  17822  cicfval  17844  initoval  18046  termoval  18047  zerooval  18048  pwsco1mhm  18857  pwsco2mhm  18858  vrmdfval  18881  ghmqusnsglem1  19310  ghmquskerlem1  19313  galactghm  19436  symgfixfolem1  19470  pmtrval  19483  pmtrfv  19484  pmtrdifwrdellem3  19515  gsummhm2  19971  gsummpt1n0  19997  dprdfid  20051  rgspnval  20628  lspval  20990  uvcval  21822  aspval  21910  evlslem3  22121  psdmplcl  22183  psdadd  22184  psdmul  22187  coe1tmfv1  22292  coe1tmfv2  22293  evls1maprhm  22395  evls1maplmhm  22396  rhmmpl  22402  rhmply1vr1  22406  rhmply1vsca  22407  mat1rhmval  22500  scmatrhmval  22548  marepvval  22588  mply1topmatval  22825  mp2pm2mplem1  22827  chfacfscmulgsum  22881  chfacfpmmulgsum  22885  tgval  22977  ntrval  23059  clsval  23060  opncldf2  23108  neival  23125  lpval  23162  1stcfb  23468  cnmpt11  23686  cnmpt21  23694  cnmptkp  23703  cnmptk1p  23708  ustval  24226  iunmbl  25601  cnmptlimc  25939  limccnp  25940  limcco  25942  coe1termlem  26311  coe1term  26312  ulmval  26437  pserulm  26479  efgh  26597  rlimcnp  27022  xrlimcnp  27025  dchrelbasd  27297  gausslemma2dlem4  27427  2lgslem1b  27450  madeval  27905  abssval  28277  tgjustr  28496  mirval  28677  midf  28798  ismidb  28800  lmif  28807  islmib  28809  wksfval  29641  crctcshwlkn0lem2  29840  crctcshwlkn0lem3  29841  wwlks  29864  wlkiswwlks2lem2  29899  wlkswwlksf1o  29908  clwwlk  30011  clwlkclwwlkf1  30038  numclwlk2lem2fv  30406  spanval  31361  fsuppcurry1  32742  fsuppcurry2  32743  mndlactf1  33013  mndlactfo  33014  mndractf1  33015  mndractfo  33016  mndlactf1o  33017  mndractf1o  33018  gsumwrd2dccat  33052  fzto1stfv1  33103  tocycval  33110  elrgspnlem1  33231  elrgspnlem2  33232  rlocf1  33259  qusrn  33416  elrspunidl  33435  elrspunsn  33436  prmidlval  33444  rprmval  33523  zringfrac  33561  ply1gsumz  33598  r1plmhm  33609  ply1degltdimlem  33649  lactlmhm  33661  evls1fldgencl  33694  ply1annidllem  33708  algextdeglem7  33728  rhmpreimacnlem  33844  indv  33992  esumcvg  34066  omsval  34274  eulerpartlemgvv  34357  cndprobval  34414  reprval  34603  hgt750lemb  34649  satfvsuc  35345  sat1el2xp  35363  fmlasuc0  35368  climlec3  35713  fwddifval  36143  knoppcnlem1  36475  knoppcnlem9  36483  unbdqndv2lem2  36492  knoppndvlem4  36497  knoppndvlem6  36499  bj-diagval  37156  bj-endval  37297  heiborlem4  37800  heiborlem6  37802  pclvalN  39872  frlmsnic  42526  rhmpsr  42538  mplmapghm  42542  evlsvvval  42549  evlsbagval  42552  evlsmaprhm  42556  evlsevl  42557  selvvvval  42571  evlselv  42573  mhphflem  42582  prjspnfv01  42610  prjspner01  42611  prjspner1  42612  rabdiophlem2  42789  fphpdo  42804  monotoddzz  42931  dnnumch3lem  43034  pwssplit4  43077  hbtlem1  43111  eliunov2  43668  fvmptiunrelexplb0d  43673  fvmptiunrelexplb1d  43675  dssmapfvd  44006  wessf1ornlem  45127  projf1o  45139  fmuldfeq  45538  clim1fr1  45556  mullimcf  45578  sumnnodd  45585  expfac  45612  fnlimfv  45618  fnlimfvre2  45632  fnlimabslt  45634  limsuplt2  45708  liminfval  45714  limsupge  45716  cncfshift  45829  cncfiooicclem1  45848  fprodsubrecnncnvlem  45862  fprodaddrecnncnvlem  45864  ioodvbdlimc1lem1  45886  ioodvbdlimc1lem2  45887  dvnmul  45898  dvnprodlem1  45901  dvnprodlem2  45902  dvnprodlem3  45903  itgsinexp  45910  stoweidlem7  45962  stoweidlem17  45972  stoweidlem26  45981  stoweidlem30  45985  stoweidlem31  45986  stoweidlem32  45987  stoweidlem34  45989  wallispilem4  46023  wallispi  46025  stirlinglem3  46031  stirlinglem5  46033  stirlinglem7  46035  stirlinglem10  46038  dirkercncflem2  46059  etransclem1  46190  etransclem12  46201  etransclem27  46216  etransclem46  46235  etransclem48  46237  sge0snmptf  46392  nnfoctbdjlem  46410  psmeasurelem  46425  psmeasure  46426  meaiuninclem  46435  meaiininclem  46441  carageniuncllem1  46476  carageniuncllem2  46477  caratheodorylem1  46481  0ome  46484  vonval  46495  ovnval  46496  ovnval2b  46507  hoiprodcl2  46510  ovnlecvr  46513  ovncvrrp  46519  ovnsubaddlem1  46525  hsphoif  46531  hoidmvval  46532  hsphoival  46534  ovnhoilem1  46556  hoidifhspval  46563  hspval  46564  ovncvr2  46566  hspmbllem2  46582  ovnsubadd2lem  46600  vonioolem2  46636  vonicclem2  46639  issmflem  46682  smflimsuplem1  46775  smflimsuplem5  46779  smflimsuplem7  46781  fvmptrabdm  47242  sprsymrelfv  47418  prproropf1olem4  47430  fmtno  47453  prmdvdsfmtnof1  47511  upwlksfval  47978  uspgrsprfv  47988  assintopval  48048  lincop  48253  linc1  48270  lincext3  48301  el0ldep  48311  lincresunit2  48323  lincresunit3lem1  48324  blenval  48420  digfval  48446  itcoval  48510  ackval0012  48538  ackval1012  48539  ackval2012  48540  ackval3012  48541  lines  48580  spheres  48595