Theorem fvmptd3 7009

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108   ↦ cmpt 5201  ‘cfv 6531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-iota 6484  df-fun 6533  df-fv 6539

This theorem is referenced by:  mptmpoopabbrd  8079  mptmpoopabbrdOLD  8080  mptmpoopabbrdOLDOLD  8082  undefval  8275  tz7.44-2  8421  fsetfocdm  8875  fvdiagfn  8905  resixpfo  8950  fival  9424  cantnfp1lem1  9692  cantnfp1lem2  9693  cantnfp1lem3  9694  wemapwe  9711  rankvalb  9811  djulcl  9924  djuss  9934  1stinl  9941  2ndinl  9942  1stinr  9943  2ndinr  9944  fin23lem27  10342  isf34lem1  10386  canthp1lem2  10667  wuncval  10756  climrlim2  15563  summolem3  15730  prodmolem3  15949  iprodmul  16019  lcmfval  16640  iserodd  16855  mreacs  17670  isofval  17770  isofn  17788  cicfval  17810  initoval  18006  termoval  18007  zerooval  18008  pwsco1mhm  18810  pwsco2mhm  18811  vrmdfval  18834  ghmqusnsglem1  19263  ghmquskerlem1  19266  galactghm  19385  symgfixfolem1  19419  pmtrval  19432  pmtrfv  19433  pmtrdifwrdellem3  19464  gsummhm2  19920  gsummpt1n0  19946  dprdfid  20000  rgspnval  20572  lspval  20932  uvcval  21745  aspval  21833  evlslem3  22038  psdmplcl  22100  psdadd  22101  psdmul  22104  psdmvr  22107  coe1tmfv1  22211  coe1tmfv2  22212  evls1maprhm  22314  evls1maplmhm  22315  rhmmpl  22321  rhmply1vr1  22325  rhmply1vsca  22326  mat1rhmval  22417  scmatrhmval  22465  marepvval  22505  mply1topmatval  22742  mp2pm2mplem1  22744  chfacfscmulgsum  22798  chfacfpmmulgsum  22802  tgval  22893  ntrval  22974  clsval  22975  opncldf2  23023  neival  23040  lpval  23077  1stcfb  23383  cnmpt11  23601  cnmpt21  23609  cnmptkp  23618  cnmptk1p  23623  ustval  24141  iunmbl  25506  cnmptlimc  25843  limccnp  25844  limcco  25846  coe1termlem  26215  coe1term  26216  ulmval  26341  pserulm  26383  efgh  26502  rlimcnp  26927  xrlimcnp  26930  dchrelbasd  27202  gausslemma2dlem4  27332  2lgslem1b  27355  madeval  27812  abssval  28193  tgjustr  28453  mirval  28634  midf  28755  ismidb  28757  lmif  28764  islmib  28766  wksfval  29589  crctcshwlkn0lem2  29793  crctcshwlkn0lem3  29794  wwlks  29817  wlkiswwlks2lem2  29852  wlkswwlksf1o  29861  clwwlk  29964  clwlkclwwlkf1  29991  numclwlk2lem2fv  30359  spanval  31314  fsuppcurry1  32702  fsuppcurry2  32703  indv  32829  mndlactf1  33021  mndlactfo  33022  mndractf1  33023  mndractfo  33024  mndlactf1o  33025  mndractf1o  33026  gsumwrd2dccat  33061  fzto1stfv1  33112  tocycval  33119  elrgspnlem1  33237  elrgspnlem2  33238  elrgspnsubrunlem2  33243  rlocf1  33268  qusrn  33424  elrspunidl  33443  elrspunsn  33444  prmidlval  33452  rprmval  33531  zringfrac  33569  ply1gsumz  33608  r1plmhm  33619  ply1degltdimlem  33662  lactlmhm  33674  evls1fldgencl  33711  fldextrspunlsplem  33714  fldextrspunlsp  33715  ply1annidllem  33735  algextdeglem7  33757  rhmpreimacnlem  33915  esumcvg  34117  omsval  34325  eulerpartlemgvv  34408  cndprobval  34465  reprval  34642  hgt750lemb  34688  satfvsuc  35383  sat1el2xp  35401  fmlasuc0  35406  climlec3  35751  fwddifval  36180  knoppcnlem1  36511  knoppcnlem9  36519  unbdqndv2lem2  36528  knoppndvlem4  36533  knoppndvlem6  36535  bj-diagval  37192  bj-endval  37333  heiborlem4  37838  heiborlem6  37840  pclvalN  39909  frlmsnic  42563  rhmpsr  42575  mplmapghm  42579  evlsvvval  42586  evlsbagval  42589  evlsmaprhm  42593  evlsevl  42594  selvvvval  42608  evlselv  42610  mhphflem  42619  prjspnfv01  42647  prjspner01  42648  prjspner1  42649  rabdiophlem2  42825  fphpdo  42840  monotoddzz  42967  dnnumch3lem  43070  pwssplit4  43113  hbtlem1  43147  eliunov2  43703  fvmptiunrelexplb0d  43708  fvmptiunrelexplb1d  43710  dssmapfvd  44041  wessf1ornlem  45209  projf1o  45221  fmuldfeq  45612  clim1fr1  45630  mullimcf  45652  sumnnodd  45659  expfac  45686  fnlimfv  45692  fnlimfvre2  45706  fnlimabslt  45708  limsuplt2  45782  liminfval  45788  limsupge  45790  cncfshift  45903  cncfiooicclem1  45922  fprodsubrecnncnvlem  45936  fprodaddrecnncnvlem  45938  ioodvbdlimc1lem1  45960  ioodvbdlimc1lem2  45961  dvnmul  45972  dvnprodlem1  45975  dvnprodlem2  45976  dvnprodlem3  45977  itgsinexp  45984  stoweidlem7  46036  stoweidlem17  46046  stoweidlem26  46055  stoweidlem30  46059  stoweidlem31  46060  stoweidlem32  46061  stoweidlem34  46063  wallispilem4  46097  wallispi  46099  stirlinglem3  46105  stirlinglem5  46107  stirlinglem7  46109  stirlinglem10  46112  dirkercncflem2  46133  etransclem1  46264  etransclem12  46275  etransclem27  46290  etransclem46  46309  etransclem48  46311  sge0snmptf  46466  nnfoctbdjlem  46484  psmeasurelem  46499  psmeasure  46500  meaiuninclem  46509  meaiininclem  46515  carageniuncllem1  46550  carageniuncllem2  46551  caratheodorylem1  46555  0ome  46558  vonval  46569  ovnval  46570  ovnval2b  46581  hoiprodcl2  46584  ovnlecvr  46587  ovncvrrp  46593  ovnsubaddlem1  46599  hsphoif  46605  hoidmvval  46606  hsphoival  46608  ovnhoilem1  46630  hoidifhspval  46637  hspval  46638  ovncvr2  46640  hspmbllem2  46656  ovnsubadd2lem  46674  vonioolem2  46710  vonicclem2  46713  issmflem  46756  smflimsuplem1  46849  smflimsuplem5  46853  smflimsuplem7  46855  fvmptrabdm  47322  sprsymrelfv  47508  prproropf1olem4  47520  fmtno  47543  prmdvdsfmtnof1  47601  upwlksfval  48110  uspgrsprfv  48120  assintopval  48180  lincop  48384  linc1  48401  lincext3  48432  el0ldep  48442  lincresunit2  48454  lincresunit3lem1  48455  blenval  48551  digfval  48577  itcoval  48641  ackval0012  48669  ackval1012  48670  ackval2012  48671  ackval3012  48672  lines  48711  spheres  48726  invfn  49000  fucoid  49259