Theorem fvmptd3 7022

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

Syntax hints:   → wi 4   = wceq 1534   ∈ wcel 2099   ↦ cmpt 5225  ‘cfv 6542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pr 5423

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ral 3057  df-rex 3066  df-rab 3428  df-v 3471  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-br 5143  df-opab 5205  df-mpt 5226  df-id 5570  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-iota 6494  df-fun 6544  df-fv 6550

This theorem is referenced by:  mptmpoopabbrd  8079  mptmpoopabbrdOLD  8080  mptmpoopabbrdOLDOLD  8082  undefval  8275  tz7.44-2  8421  fvdiagfn  8901  resixpfo  8946  fival  9427  cantnfp1lem1  9693  cantnfp1lem2  9694  cantnfp1lem3  9695  wemapwe  9712  rankvalb  9812  djulcl  9925  djuss  9935  1stinl  9942  2ndinl  9943  1stinr  9944  2ndinr  9945  fin23lem27  10343  isf34lem1  10387  canthp1lem2  10668  wuncval  10757  climrlim2  15515  summolem3  15684  prodmolem3  15901  iprodmul  15971  lcmfval  16583  iserodd  16795  mreacs  17629  isofval  17731  isofn  17749  cicfval  17771  initoval  17973  termoval  17974  zerooval  17975  pwsco1mhm  18775  pwsco2mhm  18776  vrmdfval  18799  ghmquskerlem1  19225  galactghm  19350  symgfixfolem1  19384  pmtrval  19397  pmtrfv  19398  pmtrdifwrdellem3  19429  gsummhm2  19885  gsummpt1n0  19911  dprdfid  19965  lspval  20848  uvcval  21706  aspval  21793  evlslem3  22013  psdmplcl  22073  psdadd  22074  psdmul  22077  coe1tmfv1  22180  coe1tmfv2  22181  mat1rhmval  22368  scmatrhmval  22416  marepvval  22456  mply1topmatval  22693  mp2pm2mplem1  22695  chfacfscmulgsum  22749  chfacfpmmulgsum  22753  tgval  22845  ntrval  22927  clsval  22928  opncldf2  22976  neival  22993  lpval  23030  1stcfb  23336  cnmpt11  23554  cnmpt21  23562  cnmptkp  23571  cnmptk1p  23576  ustval  24094  iunmbl  25469  cnmptlimc  25806  limccnp  25807  limcco  25809  coe1termlem  26179  coe1term  26180  ulmval  26303  pserulm  26345  efgh  26462  rlimcnp  26884  xrlimcnp  26887  dchrelbasd  27159  gausslemma2dlem4  27289  2lgslem1b  27312  madeval  27766  abssval  28120  tgjustr  28265  mirval  28446  midf  28567  ismidb  28569  lmif  28576  islmib  28578  wksfval  29410  crctcshwlkn0lem2  29609  crctcshwlkn0lem3  29610  wwlks  29633  wlkiswwlks2lem2  29668  wlkswwlksf1o  29677  clwwlk  29780  clwlkclwwlkf1  29807  numclwlk2lem2fv  30175  spanval  31130  fsuppcurry1  32491  fsuppcurry2  32492  fzto1stfv1  32800  tocycval  32807  qusrn  33059  elrspunidl  33079  elrspunsn  33080  prmidlval  33088  rprmval  33166  ply1gsumz  33201  r1plmhm  33212  ply1degltdimlem  33252  evls1fldgencl  33290  evls1maprhm  33305  evls1maplmhm  33306  ply1annidllem  33308  algextdeglem7  33327  rhmpreimacnlem  33421  indv  33567  esumcvg  33641  omsval  33849  eulerpartlemgvv  33932  cndprobval  33989  reprval  34178  hgt750lemb  34224  satfvsuc  34907  sat1el2xp  34925  fmlasuc0  34930  climlec3  35264  fwddifval  35694  knoppcnlem1  35904  knoppcnlem9  35912  unbdqndv2lem2  35921  knoppndvlem4  35926  knoppndvlem6  35928  bj-diagval  36589  bj-endval  36730  heiborlem4  37222  heiborlem6  37224  pclvalN  39300  frlmsnic  41692  rhmmpl  41708  mplmapghm  41711  evlsvvval  41718  evlsbagval  41721  evlsmaprhm  41725  evlsevl  41726  selvvvval  41740  evlselv  41742  mhphflem  41751  prjspnfv01  41970  prjspner01  41971  prjspner1  41972  rabdiophlem2  42144  fphpdo  42159  monotoddzz  42286  dnnumch3lem  42392  pwssplit4  42435  hbtlem1  42469  rgspnval  42514  eliunov2  43032  fvmptiunrelexplb0d  43037  fvmptiunrelexplb1d  43039  dssmapfvd  43370  wessf1ornlem  44481  projf1o  44493  fmuldfeq  44894  clim1fr1  44912  mullimcf  44934  sumnnodd  44941  expfac  44968  fnlimfv  44974  fnlimfvre2  44988  fnlimabslt  44990  limsuplt2  45064  liminfval  45070  limsupge  45072  cncfshift  45185  cncfiooicclem1  45204  fprodsubrecnncnvlem  45218  fprodaddrecnncnvlem  45220  ioodvbdlimc1lem1  45242  ioodvbdlimc1lem2  45243  dvnmul  45254  dvnprodlem1  45257  dvnprodlem2  45258  dvnprodlem3  45259  itgsinexp  45266  stoweidlem7  45318  stoweidlem17  45328  stoweidlem26  45337  stoweidlem30  45341  stoweidlem31  45342  stoweidlem32  45343  stoweidlem34  45345  wallispilem4  45379  wallispi  45381  stirlinglem3  45387  stirlinglem5  45389  stirlinglem7  45391  stirlinglem10  45394  dirkercncflem2  45415  etransclem1  45546  etransclem12  45557  etransclem27  45572  etransclem46  45591  etransclem48  45593  sge0snmptf  45748  nnfoctbdjlem  45766  psmeasurelem  45781  psmeasure  45782  meaiuninclem  45791  meaiininclem  45797  carageniuncllem1  45832  carageniuncllem2  45833  caratheodorylem1  45837  0ome  45840  vonval  45851  ovnval  45852  ovnval2b  45863  hoiprodcl2  45866  ovnlecvr  45869  ovncvrrp  45875  ovnsubaddlem1  45881  hsphoif  45887  hoidmvval  45888  hsphoival  45890  ovnhoilem1  45912  hoidifhspval  45919  hspval  45920  ovncvr2  45922  hspmbllem2  45938  ovnsubadd2lem  45956  vonioolem2  45992  vonicclem2  45995  issmflem  46038  smflimsuplem1  46131  smflimsuplem5  46135  smflimsuplem7  46137  fvmptrabdm  46596  sprsymrelfv  46757  prproropf1olem4  46769  fmtno  46792  prmdvdsfmtnof1  46850  upwlksfval  47120  uspgrsprfv  47130  assintopval  47190  lincop  47399  linc1  47416  lincext3  47447  el0ldep  47457  lincresunit2  47469  lincresunit3lem1  47470  blenval  47567  digfval  47593  itcoval  47657  ackval0012  47685  ackval1012  47686  ackval2012  47687  ackval3012  47688  lines  47727  spheres  47742