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  8083  undefval  8278  tz7.44-2  8399  fsetfocdm  8865  fvdiagfn  8901  resixpfo  8946  fival  9385  cantnfp1lem1  9660  cantnfp1lem2  9661  cantnfp1lem3  9662  wemapwe  9679  rankvalb  9782  djulcl  9918  djuss  9928  1stinl  9935  2ndinl  9936  1stinr  9937  2ndinr  9938  fin23lem27  10333  isf34lem1  10377  canthp1lem2  10665  wuncval  10754  indv  12247  climrlim2  15636  summolem3  15802  prodmolem3  16024  iprodmul  16094  lcmfval  16715  iserodd  16931  mreacs  17750  isofval  17850  isofn  17868  cicfval  17890  initoval  18086  termoval  18087  zerooval  18088  pwsco1mhm  18942  pwsco2mhm  18943  vrmdfval  18966  ghmqusnsglem1  19408  ghmquskerlem1  19411  galactghm  19532  symgfixfolem1  19566  pmtrval  19579  pmtrfv  19580  pmtrdifwrdellem3  19611  gsummhm2  20067  gsummpt1n0  20093  dprdfid  20147  rgspnval  20775  lspval  21160  prmidlval  21526  uvcval  21999  aspval  22088  evlslem3  22297  evlsvvval  22310  mplmapghm  22339  evlsmaprhm  22348  evlsevl  22349  selvvvval  22359  psdmplcl  22391  psdadd  22392  psdmul  22395  psdmvr  22398  coe1tmfv1  22501  coe1tmfv2  22502  evls1maprhm  22602  evls1maplmhm  22603  rhmmpl  22606  rhmply1vr1  22610  rhmply1vsca  22611  mat1rhmval  22702  scmatrhmval  22750  marepvval  22790  mply1topmatval  23030  mp2pm2mplem1  23032  chfacfscmulgsum  23086  chfacfpmmulgsum  23090  tgval  23181  ntrval  23262  clsval  23263  opncldf2  23311  neival  23328  lpval  23365  1stcfb  23671  cnmpt11  23890  cnmpt21  23898  cnmptkp  23907  cnmptk1p  23912  ustval  24430  iunmbl  25782  cnmptlimc  26119  limccnp  26120  limcco  26122  coe1termlem  26485  coe1term  26486  ulmval  26613  pserulm  26655  efgh  26776  rlimcnp  27200  xrlimcnp  27203  dchrelbasd  27473  gausslemma2dlem4  27603  2lgslem1b  27626  madeval  28095  abssval  28502  tgjustr  28813  mirval  29004  tgplnfn  29130  plngval  29132  isplng  29133  midf  29158  ismidb  29160  lmif  29167  islmib  29169  brprlng  29281  wksfval  30055  crctcshwlkn0lem2  30265  crctcshwlkn0lem3  30266  wwlks  30289  wlkiswwlks2lem2  30324  wlkswwlksf1o  30333  clwwlk  30439  clwlkclwwlkf1  30466  numclwlk2lem2fv  30844  spanval  31800  fsuppcurry1  33182  fsuppcurry2  33183  mndlactf1  33453  mndlactfo  33454  mndractf1  33455  mndractfo  33456  mndlactf1o  33457  mndractf1o  33458  gsummulsubdishift1s  33497  gsummulsubdishift2s  33498  gsumwrd2dccat  33505  fzto1stfv1  33528  tocycval  33535  fxpsubm  33599  fxpsubg  33600  fxpsubrg  33601  fxpsdrg  33602  elrgspnlem1  33669  elrgspnlem2  33670  elrgspnsubrunlem2  33675  rlocf1  33701  qusrn  33825  elrspunidl  33843  elrspunsn  33844  rprmval  33913  zringfrac  33951  ply1gsumz  33996  r1plmhm  34006  0mplrim  34011  selvply1rhmlema  34015  selvply1rhmlemb  34016  selvply1rhmlem3  34019  selvply1rhmlem5  34021  extvfvcl  34033  mplvrpmrhm  34044  psrmonmul2  34048  psrmonprod  34049  esplyfvaln  34071  vietadeg1  34075  ply1degltdimlem  34119  lactlmhm  34131  evls1fldgencl  34167  fldextrspunlsplem  34170  fldextrspunlsp  34171  ply1annidllem  34198  algextdeglem7  34220  rhmpreimacnlem  34381  esumcvg  34583  omsval  34791  eulerpartlemgvv  34874  cndprobval  34931  reprval  35105  hgt750lemb  35151  fineqvnttrclselem2  35635  fineqvnttrclselem3  35636  fineqvnttrclse  35637  satfvsuc  35927  sat1el2xp  35945  fmlasuc0  35950  climlec3  36300  fwddifval  36729  knoppcnlem1  37177  knoppcnlem9  37185  unbdqndv2lem2  37194  knoppndvlem4  37199  knoppndvlem6  37201  bj-diagval  37913  bj-endval  38054  heiborlem4  38551  heiborlem6  38553  pclvalN  40750  frlmsnic  43409  rhmpsr  43416  evlsbagval  43419  evlselv  43422  mhphflem  43429  prjspnfv01  43457  prjspner01  43458  prjspner1  43459  rabdiophlem2  43630  fphpdo  43645  monotoddzz  43771  dnnumch3lem  43874  pwssplit4  43917  hbtlem1  43951  eliunov2  44506  fvmptiunrelexplb0d  44511  fvmptiunrelexplb1d  44513  dssmapfvd  44844  wessf1ornlem  46004  projf1o  46015  fmuldfeq  46400  clim1fr1  46418  mullimcf  46440  sumnnodd  46447  expfac  46472  fnlimfv  46478  fnlimfvre2  46492  fnlimabslt  46494  limsuplt2  46568  liminfval  46574  limsupge  46576  cncfshift  46689  cncfiooicclem1  46708  fprodsubrecnncnvlem  46722  fprodaddrecnncnvlem  46724  ioodvbdlimc1lem1  46746  ioodvbdlimc1lem2  46747  dvnmul  46758  dvnprodlem1  46761  dvnprodlem2  46762  dvnprodlem3  46763  itgsinexp  46770  stoweidlem7  46822  stoweidlem17  46832  stoweidlem26  46841  stoweidlem30  46845  stoweidlem31  46846  stoweidlem32  46847  stoweidlem34  46849  wallispilem4  46883  wallispi  46885  stirlinglem3  46891  stirlinglem5  46893  stirlinglem7  46895  stirlinglem10  46898  dirkercncflem2  46919  fourierdlem48  46969  fourierdlem49  46970  etransclem1  47050  etransclem12  47061  etransclem27  47076  etransclem46  47095  etransclem48  47097  sge0snmptf  47252  nnfoctbdjlem  47270  psmeasurelem  47285  psmeasure  47286  meaiuninclem  47295  meaiininclem  47301  carageniuncllem1  47336  carageniuncllem2  47337  caratheodorylem1  47341  0ome  47344  vonval  47355  ovnval  47356  ovnval2b  47367  hoiprodcl2  47370  ovnlecvr  47373  ovncvrrp  47379  ovnsubaddlem1  47385  hsphoif  47391  hoidmvval  47392  hsphoival  47394  ovnhoilem1  47416  hoidifhspval  47423  hspval  47424  ovncvr2  47426  hspmbllem2  47442  ovnsubadd2lem  47460  vonioolem2  47496  vonicclem2  47499  issmflem  47542  smflimsuplem1  47635  smflimsuplem5  47639  smflimsuplem7  47641  tmachlem-tpitem  47755  fvmptrabdm  48168  sprsymrelfv  48381  prproropf1olem4  48393  fmtno  48419  prmdvdsfmtnof1  48477  ppivalnn  48522  upwlksfval  49038  uspgrsprfv  49048  assintopval  49107  lincop  49325  linc1  49342  lincext3  49373  el0ldep  49383  lincresunit2  49395  lincresunit3lem1  49396  blenval  49488  digfval  49514  itcoval  49578  ackval0012  49606  ackval1012  49607  ackval2012  49608  ackval3012  49609  lines  49648  spheres  49663  invfn  49943  fucoid  50261  crosspdot0lem  50783  crosspaltd  50786  crossp3d  50787  veroquadgsumlem  50803  veroquadmodzerod  50804