Theorem fvmptd3 6991

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

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

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 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-iota 6464  df-fun 6513  df-fv 6519

This theorem is referenced by:  mptmpoopabbrd  8059  mptmpoopabbrdOLD  8060  mptmpoopabbrdOLDOLD  8062  undefval  8255  tz7.44-2  8375  fsetfocdm  8834  fvdiagfn  8864  resixpfo  8909  fival  9363  cantnfp1lem1  9631  cantnfp1lem2  9632  cantnfp1lem3  9633  wemapwe  9650  rankvalb  9750  djulcl  9863  djuss  9873  1stinl  9880  2ndinl  9881  1stinr  9882  2ndinr  9883  fin23lem27  10281  isf34lem1  10325  canthp1lem2  10606  wuncval  10695  climrlim2  15513  summolem3  15680  prodmolem3  15899  iprodmul  15969  lcmfval  16591  iserodd  16806  mreacs  17619  isofval  17719  isofn  17737  cicfval  17759  initoval  17955  termoval  17956  zerooval  17957  pwsco1mhm  18759  pwsco2mhm  18760  vrmdfval  18783  ghmqusnsglem1  19212  ghmquskerlem1  19215  galactghm  19334  symgfixfolem1  19368  pmtrval  19381  pmtrfv  19382  pmtrdifwrdellem3  19413  gsummhm2  19869  gsummpt1n0  19895  dprdfid  19949  rgspnval  20521  lspval  20881  uvcval  21694  aspval  21782  evlslem3  21987  psdmplcl  22049  psdadd  22050  psdmul  22053  psdmvr  22056  coe1tmfv1  22160  coe1tmfv2  22161  evls1maprhm  22263  evls1maplmhm  22264  rhmmpl  22270  rhmply1vr1  22274  rhmply1vsca  22275  mat1rhmval  22366  scmatrhmval  22414  marepvval  22454  mply1topmatval  22691  mp2pm2mplem1  22693  chfacfscmulgsum  22747  chfacfpmmulgsum  22751  tgval  22842  ntrval  22923  clsval  22924  opncldf2  22972  neival  22989  lpval  23026  1stcfb  23332  cnmpt11  23550  cnmpt21  23558  cnmptkp  23567  cnmptk1p  23572  ustval  24090  iunmbl  25454  cnmptlimc  25791  limccnp  25792  limcco  25794  coe1termlem  26163  coe1term  26164  ulmval  26289  pserulm  26331  efgh  26450  rlimcnp  26875  xrlimcnp  26878  dchrelbasd  27150  gausslemma2dlem4  27280  2lgslem1b  27303  madeval  27760  abssval  28141  tgjustr  28401  mirval  28582  midf  28703  ismidb  28705  lmif  28712  islmib  28714  wksfval  29537  crctcshwlkn0lem2  29741  crctcshwlkn0lem3  29742  wwlks  29765  wlkiswwlks2lem2  29800  wlkswwlksf1o  29809  clwwlk  29912  clwlkclwwlkf1  29939  numclwlk2lem2fv  30307  spanval  31262  fsuppcurry1  32648  fsuppcurry2  32649  indv  32775  mndlactf1  32967  mndlactfo  32968  mndractf1  32969  mndractfo  32970  mndlactf1o  32971  mndractf1o  32972  gsumwrd2dccat  33007  fzto1stfv1  33058  tocycval  33065  fxpsubm  33129  elrgspnlem1  33193  elrgspnlem2  33194  elrgspnsubrunlem2  33199  rlocf1  33224  qusrn  33380  elrspunidl  33399  elrspunsn  33400  prmidlval  33408  rprmval  33487  zringfrac  33525  ply1gsumz  33564  r1plmhm  33575  ply1degltdimlem  33618  lactlmhm  33630  evls1fldgencl  33665  fldextrspunlsplem  33668  fldextrspunlsp  33669  ply1annidllem  33691  algextdeglem7  33713  rhmpreimacnlem  33874  esumcvg  34076  omsval  34284  eulerpartlemgvv  34367  cndprobval  34424  reprval  34601  hgt750lemb  34647  satfvsuc  35348  sat1el2xp  35366  fmlasuc0  35371  climlec3  35721  fwddifval  36150  knoppcnlem1  36481  knoppcnlem9  36489  unbdqndv2lem2  36498  knoppndvlem4  36503  knoppndvlem6  36505  bj-diagval  37162  bj-endval  37303  heiborlem4  37808  heiborlem6  37810  pclvalN  39884  frlmsnic  42528  rhmpsr  42540  mplmapghm  42544  evlsvvval  42551  evlsbagval  42554  evlsmaprhm  42558  evlsevl  42559  selvvvval  42573  evlselv  42575  mhphflem  42584  prjspnfv01  42612  prjspner01  42613  prjspner1  42614  rabdiophlem2  42790  fphpdo  42805  monotoddzz  42932  dnnumch3lem  43035  pwssplit4  43078  hbtlem1  43112  eliunov2  43668  fvmptiunrelexplb0d  43673  fvmptiunrelexplb1d  43675  dssmapfvd  44006  wessf1ornlem  45179  projf1o  45191  fmuldfeq  45581  clim1fr1  45599  mullimcf  45621  sumnnodd  45628  expfac  45655  fnlimfv  45661  fnlimfvre2  45675  fnlimabslt  45677  limsuplt2  45751  liminfval  45757  limsupge  45759  cncfshift  45872  cncfiooicclem1  45891  fprodsubrecnncnvlem  45905  fprodaddrecnncnvlem  45907  ioodvbdlimc1lem1  45929  ioodvbdlimc1lem2  45930  dvnmul  45941  dvnprodlem1  45944  dvnprodlem2  45945  dvnprodlem3  45946  itgsinexp  45953  stoweidlem7  46005  stoweidlem17  46015  stoweidlem26  46024  stoweidlem30  46028  stoweidlem31  46029  stoweidlem32  46030  stoweidlem34  46032  wallispilem4  46066  wallispi  46068  stirlinglem3  46074  stirlinglem5  46076  stirlinglem7  46078  stirlinglem10  46081  dirkercncflem2  46102  etransclem1  46233  etransclem12  46244  etransclem27  46259  etransclem46  46278  etransclem48  46280  sge0snmptf  46435  nnfoctbdjlem  46453  psmeasurelem  46468  psmeasure  46469  meaiuninclem  46478  meaiininclem  46484  carageniuncllem1  46519  carageniuncllem2  46520  caratheodorylem1  46524  0ome  46527  vonval  46538  ovnval  46539  ovnval2b  46550  hoiprodcl2  46553  ovnlecvr  46556  ovncvrrp  46562  ovnsubaddlem1  46568  hsphoif  46574  hoidmvval  46575  hsphoival  46577  ovnhoilem1  46599  hoidifhspval  46606  hspval  46607  ovncvr2  46609  hspmbllem2  46625  ovnsubadd2lem  46643  vonioolem2  46679  vonicclem2  46682  issmflem  46725  smflimsuplem1  46818  smflimsuplem5  46822  smflimsuplem7  46824  fvmptrabdm  47294  sprsymrelfv  47495  prproropf1olem4  47507  fmtno  47530  prmdvdsfmtnof1  47588  upwlksfval  48123  uspgrsprfv  48133  assintopval  48193  lincop  48397  linc1  48414  lincext3  48445  el0ldep  48455  lincresunit2  48467  lincresunit3lem1  48468  blenval  48560  digfval  48586  itcoval  48650  ackval0012  48678  ackval1012  48679  ackval2012  48680  ackval3012  48681  lines  48720  spheres  48735  invfn  49019  fucoid  49337