Theorem fvmptd3 6994

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109   ↦ cmpt 5191  ‘cfv 6514

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-iota 6467  df-fun 6516  df-fv 6522

This theorem is referenced by:  mptmpoopabbrd  8062  mptmpoopabbrdOLD  8063  mptmpoopabbrdOLDOLD  8065  undefval  8258  tz7.44-2  8378  fsetfocdm  8837  fvdiagfn  8867  resixpfo  8912  fival  9370  cantnfp1lem1  9638  cantnfp1lem2  9639  cantnfp1lem3  9640  wemapwe  9657  rankvalb  9757  djulcl  9870  djuss  9880  1stinl  9887  2ndinl  9888  1stinr  9889  2ndinr  9890  fin23lem27  10288  isf34lem1  10332  canthp1lem2  10613  wuncval  10702  climrlim2  15520  summolem3  15687  prodmolem3  15906  iprodmul  15976  lcmfval  16598  iserodd  16813  mreacs  17626  isofval  17726  isofn  17744  cicfval  17766  initoval  17962  termoval  17963  zerooval  17964  pwsco1mhm  18766  pwsco2mhm  18767  vrmdfval  18790  ghmqusnsglem1  19219  ghmquskerlem1  19222  galactghm  19341  symgfixfolem1  19375  pmtrval  19388  pmtrfv  19389  pmtrdifwrdellem3  19420  gsummhm2  19876  gsummpt1n0  19902  dprdfid  19956  rgspnval  20528  lspval  20888  uvcval  21701  aspval  21789  evlslem3  21994  psdmplcl  22056  psdadd  22057  psdmul  22060  psdmvr  22063  coe1tmfv1  22167  coe1tmfv2  22168  evls1maprhm  22270  evls1maplmhm  22271  rhmmpl  22277  rhmply1vr1  22281  rhmply1vsca  22282  mat1rhmval  22373  scmatrhmval  22421  marepvval  22461  mply1topmatval  22698  mp2pm2mplem1  22700  chfacfscmulgsum  22754  chfacfpmmulgsum  22758  tgval  22849  ntrval  22930  clsval  22931  opncldf2  22979  neival  22996  lpval  23033  1stcfb  23339  cnmpt11  23557  cnmpt21  23565  cnmptkp  23574  cnmptk1p  23579  ustval  24097  iunmbl  25461  cnmptlimc  25798  limccnp  25799  limcco  25801  coe1termlem  26170  coe1term  26171  ulmval  26296  pserulm  26338  efgh  26457  rlimcnp  26882  xrlimcnp  26885  dchrelbasd  27157  gausslemma2dlem4  27287  2lgslem1b  27310  madeval  27767  abssval  28148  tgjustr  28408  mirval  28589  midf  28710  ismidb  28712  lmif  28719  islmib  28721  wksfval  29544  crctcshwlkn0lem2  29748  crctcshwlkn0lem3  29749  wwlks  29772  wlkiswwlks2lem2  29807  wlkswwlksf1o  29816  clwwlk  29919  clwlkclwwlkf1  29946  numclwlk2lem2fv  30314  spanval  31269  fsuppcurry1  32655  fsuppcurry2  32656  indv  32782  mndlactf1  32974  mndlactfo  32975  mndractf1  32976  mndractfo  32977  mndlactf1o  32978  mndractf1o  32979  gsumwrd2dccat  33014  fzto1stfv1  33065  tocycval  33072  fxpsubm  33136  elrgspnlem1  33200  elrgspnlem2  33201  elrgspnsubrunlem2  33206  rlocf1  33231  qusrn  33387  elrspunidl  33406  elrspunsn  33407  prmidlval  33415  rprmval  33494  zringfrac  33532  ply1gsumz  33571  r1plmhm  33582  ply1degltdimlem  33625  lactlmhm  33637  evls1fldgencl  33672  fldextrspunlsplem  33675  fldextrspunlsp  33676  ply1annidllem  33698  algextdeglem7  33720  rhmpreimacnlem  33881  esumcvg  34083  omsval  34291  eulerpartlemgvv  34374  cndprobval  34431  reprval  34608  hgt750lemb  34654  satfvsuc  35355  sat1el2xp  35373  fmlasuc0  35378  climlec3  35728  fwddifval  36157  knoppcnlem1  36488  knoppcnlem9  36496  unbdqndv2lem2  36505  knoppndvlem4  36510  knoppndvlem6  36512  bj-diagval  37169  bj-endval  37310  heiborlem4  37815  heiborlem6  37817  pclvalN  39891  frlmsnic  42535  rhmpsr  42547  mplmapghm  42551  evlsvvval  42558  evlsbagval  42561  evlsmaprhm  42565  evlsevl  42566  selvvvval  42580  evlselv  42582  mhphflem  42591  prjspnfv01  42619  prjspner01  42620  prjspner1  42621  rabdiophlem2  42797  fphpdo  42812  monotoddzz  42939  dnnumch3lem  43042  pwssplit4  43085  hbtlem1  43119  eliunov2  43675  fvmptiunrelexplb0d  43680  fvmptiunrelexplb1d  43682  dssmapfvd  44013  wessf1ornlem  45186  projf1o  45198  fmuldfeq  45588  clim1fr1  45606  mullimcf  45628  sumnnodd  45635  expfac  45662  fnlimfv  45668  fnlimfvre2  45682  fnlimabslt  45684  limsuplt2  45758  liminfval  45764  limsupge  45766  cncfshift  45879  cncfiooicclem1  45898  fprodsubrecnncnvlem  45912  fprodaddrecnncnvlem  45914  ioodvbdlimc1lem1  45936  ioodvbdlimc1lem2  45937  dvnmul  45948  dvnprodlem1  45951  dvnprodlem2  45952  dvnprodlem3  45953  itgsinexp  45960  stoweidlem7  46012  stoweidlem17  46022  stoweidlem26  46031  stoweidlem30  46035  stoweidlem31  46036  stoweidlem32  46037  stoweidlem34  46039  wallispilem4  46073  wallispi  46075  stirlinglem3  46081  stirlinglem5  46083  stirlinglem7  46085  stirlinglem10  46088  dirkercncflem2  46109  etransclem1  46240  etransclem12  46251  etransclem27  46266  etransclem46  46285  etransclem48  46287  sge0snmptf  46442  nnfoctbdjlem  46460  psmeasurelem  46475  psmeasure  46476  meaiuninclem  46485  meaiininclem  46491  carageniuncllem1  46526  carageniuncllem2  46527  caratheodorylem1  46531  0ome  46534  vonval  46545  ovnval  46546  ovnval2b  46557  hoiprodcl2  46560  ovnlecvr  46563  ovncvrrp  46569  ovnsubaddlem1  46575  hsphoif  46581  hoidmvval  46582  hsphoival  46584  ovnhoilem1  46606  hoidifhspval  46613  hspval  46614  ovncvr2  46616  hspmbllem2  46632  ovnsubadd2lem  46650  vonioolem2  46686  vonicclem2  46689  issmflem  46732  smflimsuplem1  46825  smflimsuplem5  46829  smflimsuplem7  46831  fvmptrabdm  47298  sprsymrelfv  47499  prproropf1olem4  47511  fmtno  47534  prmdvdsfmtnof1  47592  upwlksfval  48127  uspgrsprfv  48137  assintopval  48197  lincop  48401  linc1  48418  lincext3  48449  el0ldep  48459  lincresunit2  48471  lincresunit3lem1  48472  blenval  48564  digfval  48590  itcoval  48654  ackval0012  48682  ackval1012  48683  ackval2012  48684  ackval3012  48685  lines  48724  spheres  48739  invfn  49023  fucoid  49341