Theorem fvmptd3 6966

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119   ↦ cmpt 5160  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-iota 6448  df-fun 6494  df-fv 6500

This theorem is referenced by:  mptmpoopabbrd  8029  undefval  8223  tz7.44-2  8343  fsetfocdm  8805  fvdiagfn  8836  resixpfo  8881  fival  9322  cantnfp1lem1  9597  cantnfp1lem2  9598  cantnfp1lem3  9599  wemapwe  9616  rankvalb  9719  djulcl  9832  djuss  9842  1stinl  9849  2ndinl  9850  1stinr  9851  2ndinr  9852  fin23lem27  10248  isf34lem1  10292  canthp1lem2  10574  wuncval  10663  indv  12159  climrlim2  15507  summolem3  15674  prodmolem3  15896  iprodmul  15966  lcmfval  16588  iserodd  16804  mreacs  17622  isofval  17722  isofn  17740  cicfval  17762  initoval  17958  termoval  17959  zerooval  17960  pwsco1mhm  18798  pwsco2mhm  18799  vrmdfval  18822  ghmqusnsglem1  19253  ghmquskerlem1  19256  galactghm  19377  symgfixfolem1  19411  pmtrval  19424  pmtrfv  19425  pmtrdifwrdellem3  19456  gsummhm2  19912  gsummpt1n0  19938  dprdfid  19992  rgspnval  20591  lspval  20972  uvcval  21767  aspval  21854  evlslem3  22063  evlsvvval  22076  mplmapghm  22105  evlsmaprhm  22114  evlsevl  22115  selvvvval  22125  psdmplcl  22157  psdadd  22158  psdmul  22161  psdmvr  22164  coe1tmfv1  22267  coe1tmfv2  22268  evls1maprhm  22369  evls1maplmhm  22370  rhmmpl  22373  rhmply1vr1  22377  rhmply1vsca  22378  mat1rhmval  22469  scmatrhmval  22517  marepvval  22557  mply1topmatval  22794  mp2pm2mplem1  22796  chfacfscmulgsum  22850  chfacfpmmulgsum  22854  tgval  22945  ntrval  23026  clsval  23027  opncldf2  23075  neival  23092  lpval  23129  1stcfb  23435  cnmpt11  23653  cnmpt21  23661  cnmptkp  23670  cnmptk1p  23675  ustval  24193  iunmbl  25545  cnmptlimc  25882  limccnp  25883  limcco  25885  coe1termlem  26248  coe1term  26249  ulmval  26370  pserulm  26412  efgh  26530  rlimcnp  26954  xrlimcnp  26957  dchrelbasd  27227  gausslemma2dlem4  27357  2lgslem1b  27380  madeval  27849  abssval  28256  tgjustr  28567  mirval  28748  midf  28869  ismidb  28871  lmif  28878  islmib  28880  wksfval  29703  crctcshwlkn0lem2  29904  crctcshwlkn0lem3  29905  wwlks  29928  wlkiswwlks2lem2  29963  wlkswwlksf1o  29972  clwwlk  30078  clwlkclwwlkf1  30105  numclwlk2lem2fv  30473  spanval  31429  fsuppcurry1  32823  fsuppcurry2  32824  mndlactf1  33112  mndlactfo  33113  mndractf1  33114  mndractfo  33115  mndlactf1o  33116  mndractf1o  33117  gsummulsubdishift1s  33158  gsummulsubdishift2s  33159  gsumwrd2dccat  33166  fzto1stfv1  33189  tocycval  33196  fxpsubm  33260  fxpsubg  33261  fxpsubrg  33262  fxpsdrg  33263  elrgspnlem1  33330  elrgspnlem2  33331  elrgspnsubrunlem2  33336  rlocf1  33361  qusrn  33499  elrspunidl  33518  elrspunsn  33519  prmidlval  33527  rprmval  33606  zringfrac  33644  ply1gsumz  33689  r1plmhm  33700  0mplrim  33705  selvply1rhmlema  33709  selvply1rhmlemb  33710  selvply1rhmlem3  33713  selvply1rhmlem5  33715  extvfvcl  33727  mplvrpmrhm  33738  psrmonmul2  33742  psrmonprod  33743  esplyfvaln  33765  vietadeg1  33769  ply1degltdimlem  33813  lactlmhm  33825  evls1fldgencl  33861  fldextrspunlsplem  33864  fldextrspunlsp  33865  ply1annidllem  33892  algextdeglem7  33914  rhmpreimacnlem  34075  esumcvg  34277  omsval  34484  eulerpartlemgvv  34567  cndprobval  34624  reprval  34801  hgt750lemb  34847  fineqvnttrclselem2  35310  fineqvnttrclselem3  35311  fineqvnttrclse  35312  satfvsuc  35596  sat1el2xp  35614  fmlasuc0  35619  climlec3  35969  fwddifval  36397  knoppcnlem1  36806  knoppcnlem9  36814  unbdqndv2lem2  36823  knoppndvlem4  36828  knoppndvlem6  36830  bj-diagval  37541  bj-endval  37682  heiborlem4  38188  heiborlem6  38190  pclvalN  40389  frlmsnic  43033  rhmpsr  43040  evlsbagval  43043  evlselv  43046  mhphflem  43053  prjspnfv01  43081  prjspner01  43082  prjspner1  43083  rabdiophlem2  43254  fphpdo  43269  monotoddzz  43395  dnnumch3lem  43498  pwssplit4  43541  hbtlem1  43575  eliunov2  44130  fvmptiunrelexplb0d  44135  fvmptiunrelexplb1d  44137  dssmapfvd  44468  wessf1ornlem  45639  projf1o  45650  fmuldfeq  46035  clim1fr1  46053  mullimcf  46075  sumnnodd  46082  expfac  46107  fnlimfv  46113  fnlimfvre2  46127  fnlimabslt  46129  limsuplt2  46203  liminfval  46209  limsupge  46211  cncfshift  46324  cncfiooicclem1  46343  fprodsubrecnncnvlem  46357  fprodaddrecnncnvlem  46359  ioodvbdlimc1lem1  46381  ioodvbdlimc1lem2  46382  dvnmul  46393  dvnprodlem1  46396  dvnprodlem2  46397  dvnprodlem3  46398  itgsinexp  46405  stoweidlem7  46457  stoweidlem17  46467  stoweidlem26  46476  stoweidlem30  46480  stoweidlem31  46481  stoweidlem32  46482  stoweidlem34  46484  wallispilem4  46518  wallispi  46520  stirlinglem3  46526  stirlinglem5  46528  stirlinglem7  46530  stirlinglem10  46533  dirkercncflem2  46554  etransclem1  46685  etransclem12  46696  etransclem27  46711  etransclem46  46730  etransclem48  46732  sge0snmptf  46887  nnfoctbdjlem  46905  psmeasurelem  46920  psmeasure  46921  meaiuninclem  46930  meaiininclem  46936  carageniuncllem1  46971  carageniuncllem2  46972  caratheodorylem1  46976  0ome  46979  vonval  46990  ovnval  46991  ovnval2b  47002  hoiprodcl2  47005  ovnlecvr  47008  ovncvrrp  47014  ovnsubaddlem1  47020  hsphoif  47026  hoidmvval  47027  hsphoival  47029  ovnhoilem1  47051  hoidifhspval  47058  hspval  47059  ovncvr2  47061  hspmbllem2  47077  ovnsubadd2lem  47095  vonioolem2  47131  vonicclem2  47134  issmflem  47177  smflimsuplem1  47270  smflimsuplem5  47274  smflimsuplem7  47276  fvmptrabdm  47763  sprsymrelfv  47976  prproropf1olem4  47988  fmtno  48014  prmdvdsfmtnof1  48072  ppivalnn  48117  upwlksfval  48633  uspgrsprfv  48643  assintopval  48703  lincop  48906  linc1  48923  lincext3  48954  el0ldep  48964  lincresunit2  48976  lincresunit3lem1  48977  blenval  49069  digfval  49095  itcoval  49159  ackval0012  49187  ackval1012  49188  ackval2012  49189  ackval3012  49190  lines  49229  spheres  49244  invfn  49527  fucoid  49845