Theorem fvmptd3 6964

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113   ↦ cmpt 5179  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-iota 6448  df-fun 6494  df-fv 6500

This theorem is referenced by:  mptmpoopabbrd  8024  mptmpoopabbrdOLD  8025  undefval  8218  tz7.44-2  8338  fsetfocdm  8798  fvdiagfn  8829  resixpfo  8874  fival  9315  cantnfp1lem1  9587  cantnfp1lem2  9588  cantnfp1lem3  9589  wemapwe  9606  rankvalb  9709  djulcl  9822  djuss  9832  1stinl  9839  2ndinl  9840  1stinr  9841  2ndinr  9842  fin23lem27  10238  isf34lem1  10282  canthp1lem2  10564  wuncval  10653  climrlim2  15470  summolem3  15637  prodmolem3  15856  iprodmul  15926  lcmfval  16548  iserodd  16763  mreacs  17581  isofval  17681  isofn  17699  cicfval  17721  initoval  17917  termoval  17918  zerooval  17919  pwsco1mhm  18757  pwsco2mhm  18758  vrmdfval  18781  ghmqusnsglem1  19209  ghmquskerlem1  19212  galactghm  19333  symgfixfolem1  19367  pmtrval  19380  pmtrfv  19381  pmtrdifwrdellem3  19412  gsummhm2  19868  gsummpt1n0  19894  dprdfid  19948  rgspnval  20545  lspval  20926  uvcval  21740  aspval  21828  evlslem3  22035  evlsvvval  22048  psdmplcl  22105  psdadd  22106  psdmul  22109  psdmvr  22112  coe1tmfv1  22216  coe1tmfv2  22217  evls1maprhm  22320  evls1maplmhm  22321  rhmmpl  22327  rhmply1vr1  22331  rhmply1vsca  22332  mat1rhmval  22423  scmatrhmval  22471  marepvval  22511  mply1topmatval  22748  mp2pm2mplem1  22750  chfacfscmulgsum  22804  chfacfpmmulgsum  22808  tgval  22899  ntrval  22980  clsval  22981  opncldf2  23029  neival  23046  lpval  23083  1stcfb  23389  cnmpt11  23607  cnmpt21  23615  cnmptkp  23624  cnmptk1p  23629  ustval  24147  iunmbl  25510  cnmptlimc  25847  limccnp  25848  limcco  25850  coe1termlem  26219  coe1term  26220  ulmval  26345  pserulm  26387  efgh  26506  rlimcnp  26931  xrlimcnp  26934  dchrelbasd  27206  gausslemma2dlem4  27336  2lgslem1b  27359  madeval  27828  abssval  28235  tgjustr  28546  mirval  28727  midf  28848  ismidb  28850  lmif  28857  islmib  28859  wksfval  29683  crctcshwlkn0lem2  29884  crctcshwlkn0lem3  29885  wwlks  29908  wlkiswwlks2lem2  29943  wlkswwlksf1o  29952  clwwlk  30058  clwlkclwwlkf1  30085  numclwlk2lem2fv  30453  spanval  31408  fsuppcurry1  32803  fsuppcurry2  32804  indv  32931  mndlactf1  33108  mndlactfo  33109  mndractf1  33110  mndractfo  33111  mndlactf1o  33112  mndractf1o  33113  gsummulsubdishift1s  33153  gsummulsubdishift2s  33154  gsumwrd2dccat  33160  fzto1stfv1  33183  tocycval  33190  fxpsubm  33254  fxpsubg  33255  fxpsubrg  33256  fxpsdrg  33257  elrgspnlem1  33324  elrgspnlem2  33325  elrgspnsubrunlem2  33330  rlocf1  33355  qusrn  33490  elrspunidl  33509  elrspunsn  33510  prmidlval  33518  rprmval  33597  zringfrac  33635  ply1gsumz  33680  r1plmhm  33691  extvfvcl  33701  mplvrpmrhm  33712  vietadeg1  33734  ply1degltdimlem  33779  lactlmhm  33791  evls1fldgencl  33827  fldextrspunlsplem  33830  fldextrspunlsp  33831  ply1annidllem  33858  algextdeglem7  33880  rhmpreimacnlem  34041  esumcvg  34243  omsval  34450  eulerpartlemgvv  34533  cndprobval  34590  reprval  34767  hgt750lemb  34813  fineqvnttrclselem2  35278  fineqvnttrclselem3  35279  fineqvnttrclse  35280  satfvsuc  35555  sat1el2xp  35573  fmlasuc0  35578  climlec3  35928  fwddifval  36356  knoppcnlem1  36693  knoppcnlem9  36701  unbdqndv2lem2  36710  knoppndvlem4  36715  knoppndvlem6  36717  bj-diagval  37379  bj-endval  37520  heiborlem4  38015  heiborlem6  38017  pclvalN  40150  frlmsnic  42795  rhmpsr  42805  mplmapghm  42807  evlsbagval  42812  evlsmaprhm  42816  evlsevl  42817  selvvvval  42828  evlselv  42830  mhphflem  42839  prjspnfv01  42867  prjspner01  42868  prjspner1  42869  rabdiophlem2  43044  fphpdo  43059  monotoddzz  43185  dnnumch3lem  43288  pwssplit4  43331  hbtlem1  43365  eliunov2  43920  fvmptiunrelexplb0d  43925  fvmptiunrelexplb1d  43927  dssmapfvd  44258  wessf1ornlem  45429  projf1o  45441  fmuldfeq  45829  clim1fr1  45847  mullimcf  45869  sumnnodd  45876  expfac  45901  fnlimfv  45907  fnlimfvre2  45921  fnlimabslt  45923  limsuplt2  45997  liminfval  46003  limsupge  46005  cncfshift  46118  cncfiooicclem1  46137  fprodsubrecnncnvlem  46151  fprodaddrecnncnvlem  46153  ioodvbdlimc1lem1  46175  ioodvbdlimc1lem2  46176  dvnmul  46187  dvnprodlem1  46190  dvnprodlem2  46191  dvnprodlem3  46192  itgsinexp  46199  stoweidlem7  46251  stoweidlem17  46261  stoweidlem26  46270  stoweidlem30  46274  stoweidlem31  46275  stoweidlem32  46276  stoweidlem34  46278  wallispilem4  46312  wallispi  46314  stirlinglem3  46320  stirlinglem5  46322  stirlinglem7  46324  stirlinglem10  46327  dirkercncflem2  46348  etransclem1  46479  etransclem12  46490  etransclem27  46505  etransclem46  46524  etransclem48  46526  sge0snmptf  46681  nnfoctbdjlem  46699  psmeasurelem  46714  psmeasure  46715  meaiuninclem  46724  meaiininclem  46730  carageniuncllem1  46765  carageniuncllem2  46766  caratheodorylem1  46770  0ome  46773  vonval  46784  ovnval  46785  ovnval2b  46796  hoiprodcl2  46799  ovnlecvr  46802  ovncvrrp  46808  ovnsubaddlem1  46814  hsphoif  46820  hoidmvval  46821  hsphoival  46823  ovnhoilem1  46845  hoidifhspval  46852  hspval  46853  ovncvr2  46855  hspmbllem2  46871  ovnsubadd2lem  46889  vonioolem2  46925  vonicclem2  46928  issmflem  46971  smflimsuplem1  47064  smflimsuplem5  47068  smflimsuplem7  47070  fvmptrabdm  47539  sprsymrelfv  47740  prproropf1olem4  47752  fmtno  47775  prmdvdsfmtnof1  47833  upwlksfval  48381  uspgrsprfv  48391  assintopval  48451  lincop  48654  linc1  48671  lincext3  48702  el0ldep  48712  lincresunit2  48724  lincresunit3lem1  48725  blenval  48817  digfval  48843  itcoval  48907  ackval0012  48935  ackval1012  48936  ackval2012  48937  ackval3012  48938  lines  48977  spheres  48992  invfn  49275  fucoid  49593