Theorem fvmptd3 6971

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   ↦ cmpt 5166  ‘cfv 6498

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-iota 6454  df-fun 6500  df-fv 6506

This theorem is referenced by:  mptmpoopabbrd  8033  undefval  8226  tz7.44-2  8346  fsetfocdm  8808  fvdiagfn  8839  resixpfo  8884  fival  9325  cantnfp1lem1  9599  cantnfp1lem2  9600  cantnfp1lem3  9601  wemapwe  9618  rankvalb  9721  djulcl  9834  djuss  9844  1stinl  9851  2ndinl  9852  1stinr  9853  2ndinr  9854  fin23lem27  10250  isf34lem1  10294  canthp1lem2  10576  wuncval  10665  indv  12161  climrlim2  15509  summolem3  15676  prodmolem3  15898  iprodmul  15968  lcmfval  16590  iserodd  16806  mreacs  17624  isofval  17724  isofn  17742  cicfval  17764  initoval  17960  termoval  17961  zerooval  17962  pwsco1mhm  18800  pwsco2mhm  18801  vrmdfval  18824  ghmqusnsglem1  19255  ghmquskerlem1  19258  galactghm  19379  symgfixfolem1  19413  pmtrval  19426  pmtrfv  19427  pmtrdifwrdellem3  19458  gsummhm2  19914  gsummpt1n0  19940  dprdfid  19994  rgspnval  20589  lspval  20970  uvcval  21765  aspval  21852  evlslem3  22058  evlsvvval  22071  psdmplcl  22128  psdadd  22129  psdmul  22132  psdmvr  22135  coe1tmfv1  22239  coe1tmfv2  22240  evls1maprhm  22341  evls1maplmhm  22342  rhmmpl  22348  rhmply1vr1  22352  rhmply1vsca  22353  mat1rhmval  22444  scmatrhmval  22492  marepvval  22532  mply1topmatval  22769  mp2pm2mplem1  22771  chfacfscmulgsum  22825  chfacfpmmulgsum  22829  tgval  22920  ntrval  23001  clsval  23002  opncldf2  23050  neival  23067  lpval  23104  1stcfb  23410  cnmpt11  23628  cnmpt21  23636  cnmptkp  23645  cnmptk1p  23650  ustval  24168  iunmbl  25520  cnmptlimc  25857  limccnp  25858  limcco  25860  coe1termlem  26223  coe1term  26224  ulmval  26345  pserulm  26387  efgh  26505  rlimcnp  26929  xrlimcnp  26932  dchrelbasd  27202  gausslemma2dlem4  27332  2lgslem1b  27355  madeval  27824  abssval  28231  tgjustr  28542  mirval  28723  midf  28844  ismidb  28846  lmif  28853  islmib  28855  wksfval  29678  crctcshwlkn0lem2  29879  crctcshwlkn0lem3  29880  wwlks  29903  wlkiswwlks2lem2  29938  wlkswwlksf1o  29947  clwwlk  30053  clwlkclwwlkf1  30080  numclwlk2lem2fv  30448  spanval  31404  fsuppcurry1  32797  fsuppcurry2  32798  mndlactf1  33086  mndlactfo  33087  mndractf1  33088  mndractfo  33089  mndlactf1o  33090  mndractf1o  33091  gsummulsubdishift1s  33131  gsummulsubdishift2s  33132  gsumwrd2dccat  33139  fzto1stfv1  33162  tocycval  33169  fxpsubm  33233  fxpsubg  33234  fxpsubrg  33235  fxpsdrg  33236  elrgspnlem1  33303  elrgspnlem2  33304  elrgspnsubrunlem2  33309  rlocf1  33334  qusrn  33469  elrspunidl  33488  elrspunsn  33489  prmidlval  33497  rprmval  33576  zringfrac  33614  ply1gsumz  33659  r1plmhm  33670  extvfvcl  33680  mplvrpmrhm  33691  psrmonmul2  33695  psrmonprod  33696  esplyfvaln  33718  vietadeg1  33722  ply1degltdimlem  33766  lactlmhm  33778  evls1fldgencl  33814  fldextrspunlsplem  33817  fldextrspunlsp  33818  ply1annidllem  33845  algextdeglem7  33867  rhmpreimacnlem  34028  esumcvg  34230  omsval  34437  eulerpartlemgvv  34520  cndprobval  34577  reprval  34754  hgt750lemb  34800  fineqvnttrclselem2  35266  fineqvnttrclselem3  35267  fineqvnttrclse  35268  satfvsuc  35543  sat1el2xp  35561  fmlasuc0  35566  climlec3  35916  fwddifval  36344  knoppcnlem1  36753  knoppcnlem9  36761  unbdqndv2lem2  36770  knoppndvlem4  36775  knoppndvlem6  36777  bj-diagval  37488  bj-endval  37629  heiborlem4  38135  heiborlem6  38137  pclvalN  40336  frlmsnic  42985  rhmpsr  42995  mplmapghm  42997  evlsbagval  43002  evlsmaprhm  43006  evlsevl  43007  selvvvval  43018  evlselv  43020  mhphflem  43029  prjspnfv01  43057  prjspner01  43058  prjspner1  43059  rabdiophlem2  43230  fphpdo  43245  monotoddzz  43371  dnnumch3lem  43474  pwssplit4  43517  hbtlem1  43551  eliunov2  44106  fvmptiunrelexplb0d  44111  fvmptiunrelexplb1d  44113  dssmapfvd  44444  wessf1ornlem  45615  projf1o  45626  fmuldfeq  46013  clim1fr1  46031  mullimcf  46053  sumnnodd  46060  expfac  46085  fnlimfv  46091  fnlimfvre2  46105  fnlimabslt  46107  limsuplt2  46181  liminfval  46187  limsupge  46189  cncfshift  46302  cncfiooicclem1  46321  fprodsubrecnncnvlem  46335  fprodaddrecnncnvlem  46337  ioodvbdlimc1lem1  46359  ioodvbdlimc1lem2  46360  dvnmul  46371  dvnprodlem1  46374  dvnprodlem2  46375  dvnprodlem3  46376  itgsinexp  46383  stoweidlem7  46435  stoweidlem17  46445  stoweidlem26  46454  stoweidlem30  46458  stoweidlem31  46459  stoweidlem32  46460  stoweidlem34  46462  wallispilem4  46496  wallispi  46498  stirlinglem3  46504  stirlinglem5  46506  stirlinglem7  46508  stirlinglem10  46511  dirkercncflem2  46532  etransclem1  46663  etransclem12  46674  etransclem27  46689  etransclem46  46708  etransclem48  46710  sge0snmptf  46865  nnfoctbdjlem  46883  psmeasurelem  46898  psmeasure  46899  meaiuninclem  46908  meaiininclem  46914  carageniuncllem1  46949  carageniuncllem2  46950  caratheodorylem1  46954  0ome  46957  vonval  46968  ovnval  46969  ovnval2b  46980  hoiprodcl2  46983  ovnlecvr  46986  ovncvrrp  46992  ovnsubaddlem1  46998  hsphoif  47004  hoidmvval  47005  hsphoival  47007  ovnhoilem1  47029  hoidifhspval  47036  hspval  47037  ovncvr2  47039  hspmbllem2  47055  ovnsubadd2lem  47073  vonioolem2  47109  vonicclem2  47112  issmflem  47155  smflimsuplem1  47248  smflimsuplem5  47252  smflimsuplem7  47254  fvmptrabdm  47741  sprsymrelfv  47954  prproropf1olem4  47966  fmtno  47992  prmdvdsfmtnof1  48050  ppivalnn  48095  upwlksfval  48611  uspgrsprfv  48621  assintopval  48681  lincop  48884  linc1  48901  lincext3  48932  el0ldep  48942  lincresunit2  48954  lincresunit3lem1  48955  blenval  49047  digfval  49073  itcoval  49137  ackval0012  49165  ackval1012  49166  ackval2012  49167  ackval3012  49168  lines  49207  spheres  49222  invfn  49505  fucoid  49823