Theorem fvmptd3 7003

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

Syntax hints:   → wi 4   = wceq 1563   ∈ wcel 2145   ↦ cmpt 5185  ‘cfv 6525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5250  ax-pr 5394

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5105  df-opab 5167  df-mpt 5186  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-iota 6481  df-fun 6527  df-fv 6533

This theorem is referenced by:  mptmpoopabbrd  8066  undefval  8261  tz7.44-2  8382  fsetfocdm  8846  fvdiagfn  8877  resixpfo  8922  fival  9360  cantnfp1lem1  9635  cantnfp1lem2  9636  cantnfp1lem3  9637  wemapwe  9654  rankvalb  9757  djulcl  9884  djuss  9894  1stinl  9901  2ndinl  9902  1stinr  9903  2ndinr  9904  fin23lem27  10300  isf34lem1  10344  canthp1lem2  10626  wuncval  10715  indv  12208  climrlim2  15586  summolem3  15753  prodmolem3  15975  iprodmul  16045  lcmfval  16667  iserodd  16883  mreacs  17702  isofval  17802  isofn  17820  cicfval  17842  initoval  18038  termoval  18039  zerooval  18040  pwsco1mhm  18879  pwsco2mhm  18880  vrmdfval  18903  ghmqusnsglem1  19338  ghmquskerlem1  19341  galactghm  19462  symgfixfolem1  19496  pmtrval  19509  pmtrfv  19510  pmtrdifwrdellem3  19541  gsummhm2  19997  gsummpt1n0  20023  dprdfid  20077  rgspnval  20685  lspval  21062  prmidlval  21421  uvcval  21892  aspval  21979  evlslem3  22188  evlsvvval  22201  mplmapghm  22230  evlsmaprhm  22239  evlsevl  22240  selvvvval  22250  psdmplcl  22282  psdadd  22283  psdmul  22286  psdmvr  22289  coe1tmfv1  22392  coe1tmfv2  22393  evls1maprhm  22493  evls1maplmhm  22494  rhmmpl  22497  rhmply1vr1  22501  rhmply1vsca  22502  mat1rhmval  22593  scmatrhmval  22641  marepvval  22681  mply1topmatval  22918  mp2pm2mplem1  22920  chfacfscmulgsum  22974  chfacfpmmulgsum  22978  tgval  23069  ntrval  23150  clsval  23151  opncldf2  23199  neival  23216  lpval  23253  1stcfb  23559  cnmpt11  23777  cnmpt21  23785  cnmptkp  23794  cnmptk1p  23799  ustval  24317  iunmbl  25669  cnmptlimc  26006  limccnp  26007  limcco  26009  coe1termlem  26372  coe1term  26373  ulmval  26497  pserulm  26539  efgh  26660  rlimcnp  27084  xrlimcnp  27087  dchrelbasd  27357  gausslemma2dlem4  27487  2lgslem1b  27510  madeval  27979  abssval  28386  tgjustr  28697  mirval  28882  tgplnfn  29001  plngval  29003  isplng  29004  midf  29024  ismidb  29026  lmif  29033  islmib  29035  brprlng  29119  wksfval  29864  crctcshwlkn0lem2  30065  crctcshwlkn0lem3  30066  wwlks  30089  wlkiswwlks2lem2  30124  wlkswwlksf1o  30133  clwwlk  30239  clwlkclwwlkf1  30266  numclwlk2lem2fv  30634  spanval  31590  fsuppcurry1  32977  fsuppcurry2  32978  mndlactf1  33254  mndlactfo  33255  mndractf1  33256  mndractfo  33257  mndlactf1o  33258  mndractf1o  33259  gsummulsubdishift1s  33298  gsummulsubdishift2s  33299  gsumwrd2dccat  33306  fzto1stfv1  33329  tocycval  33336  fxpsubm  33400  fxpsubg  33401  fxpsubrg  33402  fxpsdrg  33403  elrgspnlem1  33470  elrgspnlem2  33471  elrgspnsubrunlem2  33476  rlocf1  33502  qusrn  33629  elrspunidl  33647  elrspunsn  33648  rprmval  33718  zringfrac  33756  ply1gsumz  33801  r1plmhm  33811  0mplrim  33816  selvply1rhmlema  33820  selvply1rhmlemb  33821  selvply1rhmlem3  33824  selvply1rhmlem5  33826  extvfvcl  33838  mplvrpmrhm  33849  psrmonmul2  33853  psrmonprod  33854  esplyfvaln  33876  vietadeg1  33880  ply1degltdimlem  33924  lactlmhm  33936  evls1fldgencl  33972  fldextrspunlsplem  33975  fldextrspunlsp  33976  ply1annidllem  34003  algextdeglem7  34025  rhmpreimacnlem  34186  esumcvg  34388  omsval  34595  eulerpartlemgvv  34678  cndprobval  34735  reprval  34909  hgt750lemb  34955  fineqvnttrclselem2  35425  fineqvnttrclselem3  35426  fineqvnttrclse  35427  satfvsuc  35719  sat1el2xp  35737  fmlasuc0  35742  climlec3  36092  fwddifval  36520  knoppcnlem1  36939  knoppcnlem9  36947  unbdqndv2lem2  36956  knoppndvlem4  36961  knoppndvlem6  36963  bj-diagval  37673  bj-endval  37814  heiborlem4  38320  heiborlem6  38322  pclvalN  40521  frlmsnic  43165  rhmpsr  43172  evlsbagval  43175  evlselv  43178  mhphflem  43185  prjspnfv01  43213  prjspner01  43214  prjspner1  43215  rabdiophlem2  43386  fphpdo  43401  monotoddzz  43527  dnnumch3lem  43630  pwssplit4  43673  hbtlem1  43707  eliunov2  44262  fvmptiunrelexplb0d  44267  fvmptiunrelexplb1d  44269  dssmapfvd  44600  wessf1ornlem  45762  projf1o  45773  fmuldfeq  46158  clim1fr1  46176  mullimcf  46198  sumnnodd  46205  expfac  46230  fnlimfv  46236  fnlimfvre2  46250  fnlimabslt  46252  limsuplt2  46326  liminfval  46332  limsupge  46334  cncfshift  46447  cncfiooicclem1  46466  fprodsubrecnncnvlem  46480  fprodaddrecnncnvlem  46482  ioodvbdlimc1lem1  46504  ioodvbdlimc1lem2  46505  dvnmul  46516  dvnprodlem1  46519  dvnprodlem2  46520  dvnprodlem3  46521  itgsinexp  46528  stoweidlem7  46580  stoweidlem17  46590  stoweidlem26  46599  stoweidlem30  46603  stoweidlem31  46604  stoweidlem32  46605  stoweidlem34  46607  wallispilem4  46641  wallispi  46643  stirlinglem3  46649  stirlinglem5  46651  stirlinglem7  46653  stirlinglem10  46656  dirkercncflem2  46677  fourierdlem48  46727  fourierdlem49  46728  etransclem1  46808  etransclem12  46819  etransclem27  46834  etransclem46  46853  etransclem48  46855  sge0snmptf  47010  nnfoctbdjlem  47028  psmeasurelem  47043  psmeasure  47044  meaiuninclem  47053  meaiininclem  47059  carageniuncllem1  47094  carageniuncllem2  47095  caratheodorylem1  47099  0ome  47102  vonval  47113  ovnval  47114  ovnval2b  47125  hoiprodcl2  47128  ovnlecvr  47131  ovncvrrp  47137  ovnsubaddlem1  47143  hsphoif  47149  hoidmvval  47150  hsphoival  47152  ovnhoilem1  47174  hoidifhspval  47181  hspval  47182  ovncvr2  47184  hspmbllem2  47200  ovnsubadd2lem  47218  vonioolem2  47254  vonicclem2  47257  issmflem  47300  smflimsuplem1  47393  smflimsuplem5  47397  smflimsuplem7  47399  fvmptrabdm  47886  sprsymrelfv  48099  prproropf1olem4  48111  fmtno  48137  prmdvdsfmtnof1  48195  ppivalnn  48240  upwlksfval  48756  uspgrsprfv  48766  assintopval  48826  lincop  49040  linc1  49057  lincext3  49088  el0ldep  49098  lincresunit2  49110  lincresunit3lem1  49111  blenval  49203  digfval  49229  itcoval  49293  ackval0012  49321  ackval1012  49322  ackval2012  49323  ackval3012  49324  lines  49363  spheres  49378  invfn  49660  fucoid  49978