Theorem fvmptd3 6993

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

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

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 5253  ax-nul 5263  ax-pr 5389

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 3919  df-un 3921  df-ss 3933  df-nul 4299  df-if 4491  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5110  df-opab 5172  df-mpt 5191  df-id 5535  df-xp 5646  df-rel 5647  df-cnv 5648  df-co 5649  df-dm 5650  df-iota 6466  df-fun 6515  df-fv 6521

This theorem is referenced by:  mptmpoopabbrd  8061  mptmpoopabbrdOLD  8062  mptmpoopabbrdOLDOLD  8064  undefval  8257  tz7.44-2  8377  fsetfocdm  8836  fvdiagfn  8866  resixpfo  8911  fival  9369  cantnfp1lem1  9637  cantnfp1lem2  9638  cantnfp1lem3  9639  wemapwe  9656  rankvalb  9756  djulcl  9869  djuss  9879  1stinl  9886  2ndinl  9887  1stinr  9888  2ndinr  9889  fin23lem27  10287  isf34lem1  10331  canthp1lem2  10612  wuncval  10701  climrlim2  15519  summolem3  15686  prodmolem3  15905  iprodmul  15975  lcmfval  16597  iserodd  16812  mreacs  17625  isofval  17725  isofn  17743  cicfval  17765  initoval  17961  termoval  17962  zerooval  17963  pwsco1mhm  18765  pwsco2mhm  18766  vrmdfval  18789  ghmqusnsglem1  19218  ghmquskerlem1  19221  galactghm  19340  symgfixfolem1  19374  pmtrval  19387  pmtrfv  19388  pmtrdifwrdellem3  19419  gsummhm2  19875  gsummpt1n0  19901  dprdfid  19955  rgspnval  20527  lspval  20887  uvcval  21700  aspval  21788  evlslem3  21993  psdmplcl  22055  psdadd  22056  psdmul  22059  psdmvr  22062  coe1tmfv1  22166  coe1tmfv2  22167  evls1maprhm  22269  evls1maplmhm  22270  rhmmpl  22276  rhmply1vr1  22280  rhmply1vsca  22281  mat1rhmval  22372  scmatrhmval  22420  marepvval  22460  mply1topmatval  22697  mp2pm2mplem1  22699  chfacfscmulgsum  22753  chfacfpmmulgsum  22757  tgval  22848  ntrval  22929  clsval  22930  opncldf2  22978  neival  22995  lpval  23032  1stcfb  23338  cnmpt11  23556  cnmpt21  23564  cnmptkp  23573  cnmptk1p  23578  ustval  24096  iunmbl  25460  cnmptlimc  25797  limccnp  25798  limcco  25800  coe1termlem  26169  coe1term  26170  ulmval  26295  pserulm  26337  efgh  26456  rlimcnp  26881  xrlimcnp  26884  dchrelbasd  27156  gausslemma2dlem4  27286  2lgslem1b  27309  madeval  27766  abssval  28147  tgjustr  28407  mirval  28588  midf  28709  ismidb  28711  lmif  28718  islmib  28720  wksfval  29543  crctcshwlkn0lem2  29747  crctcshwlkn0lem3  29748  wwlks  29771  wlkiswwlks2lem2  29806  wlkswwlksf1o  29815  clwwlk  29918  clwlkclwwlkf1  29945  numclwlk2lem2fv  30313  spanval  31268  fsuppcurry1  32654  fsuppcurry2  32655  indv  32781  mndlactf1  32973  mndlactfo  32974  mndractf1  32975  mndractfo  32976  mndlactf1o  32977  mndractf1o  32978  gsumwrd2dccat  33013  fzto1stfv1  33064  tocycval  33071  fxpsubm  33135  elrgspnlem1  33199  elrgspnlem2  33200  elrgspnsubrunlem2  33205  rlocf1  33230  qusrn  33386  elrspunidl  33405  elrspunsn  33406  prmidlval  33414  rprmval  33493  zringfrac  33531  ply1gsumz  33570  r1plmhm  33581  ply1degltdimlem  33624  lactlmhm  33636  evls1fldgencl  33671  fldextrspunlsplem  33674  fldextrspunlsp  33675  ply1annidllem  33697  algextdeglem7  33719  rhmpreimacnlem  33880  esumcvg  34082  omsval  34290  eulerpartlemgvv  34373  cndprobval  34430  reprval  34607  hgt750lemb  34653  satfvsuc  35348  sat1el2xp  35366  fmlasuc0  35371  climlec3  35716  fwddifval  36145  knoppcnlem1  36476  knoppcnlem9  36484  unbdqndv2lem2  36493  knoppndvlem4  36498  knoppndvlem6  36500  bj-diagval  37157  bj-endval  37298  heiborlem4  37803  heiborlem6  37805  pclvalN  39879  frlmsnic  42521  rhmpsr  42533  mplmapghm  42537  evlsvvval  42544  evlsbagval  42547  evlsmaprhm  42551  evlsevl  42552  selvvvval  42566  evlselv  42568  mhphflem  42577  prjspnfv01  42605  prjspner01  42606  prjspner1  42607  rabdiophlem2  42783  fphpdo  42798  monotoddzz  42925  dnnumch3lem  43028  pwssplit4  43071  hbtlem1  43105  eliunov2  43661  fvmptiunrelexplb0d  43666  fvmptiunrelexplb1d  43668  dssmapfvd  43999  wessf1ornlem  45172  projf1o  45184  fmuldfeq  45574  clim1fr1  45592  mullimcf  45614  sumnnodd  45621  expfac  45648  fnlimfv  45654  fnlimfvre2  45668  fnlimabslt  45670  limsuplt2  45744  liminfval  45750  limsupge  45752  cncfshift  45865  cncfiooicclem1  45884  fprodsubrecnncnvlem  45898  fprodaddrecnncnvlem  45900  ioodvbdlimc1lem1  45922  ioodvbdlimc1lem2  45923  dvnmul  45934  dvnprodlem1  45937  dvnprodlem2  45938  dvnprodlem3  45939  itgsinexp  45946  stoweidlem7  45998  stoweidlem17  46008  stoweidlem26  46017  stoweidlem30  46021  stoweidlem31  46022  stoweidlem32  46023  stoweidlem34  46025  wallispilem4  46059  wallispi  46061  stirlinglem3  46067  stirlinglem5  46069  stirlinglem7  46071  stirlinglem10  46074  dirkercncflem2  46095  etransclem1  46226  etransclem12  46237  etransclem27  46252  etransclem46  46271  etransclem48  46273  sge0snmptf  46428  nnfoctbdjlem  46446  psmeasurelem  46461  psmeasure  46462  meaiuninclem  46471  meaiininclem  46477  carageniuncllem1  46512  carageniuncllem2  46513  caratheodorylem1  46517  0ome  46520  vonval  46531  ovnval  46532  ovnval2b  46543  hoiprodcl2  46546  ovnlecvr  46549  ovncvrrp  46555  ovnsubaddlem1  46561  hsphoif  46567  hoidmvval  46568  hsphoival  46570  ovnhoilem1  46592  hoidifhspval  46599  hspval  46600  ovncvr2  46602  hspmbllem2  46618  ovnsubadd2lem  46636  vonioolem2  46672  vonicclem2  46675  issmflem  46718  smflimsuplem1  46811  smflimsuplem5  46815  smflimsuplem7  46817  fvmptrabdm  47284  sprsymrelfv  47485  prproropf1olem4  47497  fmtno  47520  prmdvdsfmtnof1  47578  upwlksfval  48113  uspgrsprfv  48123  assintopval  48183  lincop  48387  linc1  48404  lincext3  48435  el0ldep  48445  lincresunit2  48457  lincresunit3lem1  48458  blenval  48550  digfval  48576  itcoval  48640  ackval0012  48668  ackval1012  48669  ackval2012  48670  ackval3012  48671  lines  48710  spheres  48725  invfn  49009  fucoid  49327