Theorem fvmptd3 7018

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106   ↦ cmpt 5230  ‘cfv 6540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-iota 6492  df-fun 6542  df-fv 6548

This theorem is referenced by:  mptmpoopabbrd  8063  mptmpoopabbrdOLD  8065  undefval  8257  tz7.44-2  8403  fvdiagfn  8881  resixpfo  8926  fival  9403  cantnfp1lem1  9669  cantnfp1lem2  9670  cantnfp1lem3  9671  wemapwe  9688  rankvalb  9788  djulcl  9901  djuss  9911  1stinl  9918  2ndinl  9919  1stinr  9920  2ndinr  9921  fin23lem27  10319  isf34lem1  10363  canthp1lem2  10644  wuncval  10733  climrlim2  15487  summolem3  15656  prodmolem3  15873  iprodmul  15943  lcmfval  16554  iserodd  16764  mreacs  17598  isofval  17700  isofn  17718  cicfval  17740  initoval  17939  termoval  17940  zerooval  17941  pwsco1mhm  18709  pwsco2mhm  18710  vrmdfval  18733  galactghm  19266  symgfixfolem1  19300  pmtrval  19313  pmtrfv  19314  pmtrdifwrdellem3  19345  gsummhm2  19801  gsummpt1n0  19827  dprdfid  19881  lspval  20578  uvcval  21331  aspval  21418  evlslem3  21634  coe1tmfv1  21787  coe1tmfv2  21788  mat1rhmval  21972  scmatrhmval  22020  marepvval  22060  mply1topmatval  22297  mp2pm2mplem1  22299  chfacfscmulgsum  22353  chfacfpmmulgsum  22357  tgval  22449  ntrval  22531  clsval  22532  opncldf2  22580  neival  22597  lpval  22634  1stcfb  22940  cnmpt11  23158  cnmpt21  23166  cnmptkp  23175  cnmptk1p  23180  ustval  23698  iunmbl  25061  cnmptlimc  25398  limccnp  25399  limcco  25401  coe1termlem  25763  coe1term  25764  ulmval  25883  pserulm  25925  efgh  26041  rlimcnp  26459  xrlimcnp  26462  dchrelbasd  26731  gausslemma2dlem4  26861  2lgslem1b  26884  madeval  27336  tgjustr  27714  mirval  27895  midf  28016  ismidb  28018  lmif  28025  islmib  28027  wksfval  28855  crctcshwlkn0lem2  29054  crctcshwlkn0lem3  29055  wwlks  29078  wlkiswwlks2lem2  29113  wlkswwlksf1o  29122  clwwlk  29225  clwlkclwwlkf1  29252  numclwlk2lem2fv  29620  spanval  30573  fsuppcurry1  31937  fsuppcurry2  31938  fzto1stfv1  32247  tocycval  32254  qusrn  32508  ghmquskerlem1  32516  elrspunidl  32534  elrspunsn  32535  prmidlval  32543  rprmval  32621  ply1gsumz  32657  ply1degltdimlem  32695  evls1maprhm  32747  evls1maplmhm  32748  ply1annidllem  32750  rhmpreimacnlem  32852  indv  32998  esumcvg  33072  omsval  33280  eulerpartlemgvv  33363  cndprobval  33420  reprval  33610  hgt750lemb  33656  satfvsuc  34340  sat1el2xp  34358  fmlasuc0  34363  climlec3  34691  fwddifval  35122  knoppcnlem1  35357  knoppcnlem9  35365  unbdqndv2lem2  35374  knoppndvlem4  35379  knoppndvlem6  35381  bj-diagval  36043  bj-endval  36184  heiborlem4  36670  heiborlem6  36672  pclvalN  38749  frlmsnic  41107  rhmmpl  41122  mplmapghm  41125  evlsvvval  41132  evlsbagval  41135  evlsmaprhm  41139  evlsevl  41140  selvvvval  41154  evlselv  41156  mhphflem  41165  prjspnfv01  41362  prjspner01  41363  prjspner1  41364  rabdiophlem2  41525  fphpdo  41540  monotoddzz  41667  dnnumch3lem  41773  pwssplit4  41816  hbtlem1  41850  rgspnval  41895  eliunov2  42415  fvmptiunrelexplb0d  42420  fvmptiunrelexplb1d  42422  dssmapfvd  42753  wessf1ornlem  43867  projf1o  43881  fmuldfeq  44285  clim1fr1  44303  mullimcf  44325  sumnnodd  44332  expfac  44359  fnlimfv  44365  fnlimfvre2  44379  fnlimabslt  44381  limsuplt2  44455  liminfval  44461  limsupge  44463  cncfshift  44576  cncfiooicclem1  44595  fprodsubrecnncnvlem  44609  fprodaddrecnncnvlem  44611  ioodvbdlimc1lem1  44633  ioodvbdlimc1lem2  44634  dvnmul  44645  dvnprodlem1  44648  dvnprodlem2  44649  dvnprodlem3  44650  itgsinexp  44657  stoweidlem7  44709  stoweidlem17  44719  stoweidlem26  44728  stoweidlem30  44732  stoweidlem31  44733  stoweidlem32  44734  stoweidlem34  44736  wallispilem4  44770  wallispi  44772  stirlinglem3  44778  stirlinglem5  44780  stirlinglem7  44782  stirlinglem10  44785  dirkercncflem2  44806  etransclem1  44937  etransclem12  44948  etransclem27  44963  etransclem46  44982  etransclem48  44984  sge0snmptf  45139  nnfoctbdjlem  45157  psmeasurelem  45172  psmeasure  45173  meaiuninclem  45182  meaiininclem  45188  carageniuncllem1  45223  carageniuncllem2  45224  caratheodorylem1  45228  0ome  45231  vonval  45242  ovnval  45243  ovnval2b  45254  hoiprodcl2  45257  ovnlecvr  45260  ovncvrrp  45266  ovnsubaddlem1  45272  hsphoif  45278  hoidmvval  45279  hsphoival  45281  ovnhoilem1  45303  hoidifhspval  45310  hspval  45311  ovncvr2  45313  hspmbllem2  45329  ovnsubadd2lem  45347  vonioolem2  45383  vonicclem2  45386  issmflem  45429  smflimsuplem1  45522  smflimsuplem5  45526  smflimsuplem7  45528  fvmptrabdm  45987  sprsymrelfv  46148  prproropf1olem4  46160  fmtno  46183  prmdvdsfmtnof1  46241  upwlksfval  46499  uspgrsprfv  46509  assintopval  46601  lincop  47042  linc1  47059  lincext3  47090  el0ldep  47100  lincresunit2  47112  lincresunit3lem1  47113  blenval  47210  digfval  47236  itcoval  47300  ackval0012  47328  ackval1012  47329  ackval2012  47330  ackval3012  47331  lines  47370  spheres  47385