Theorem fvmptd3 6791

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114   ↦ cmpt 5146  ‘cfv 6355

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-iota 6314  df-fun 6357  df-fv 6363

This theorem is referenced by:  mptmpoopabbrd  7778  undefval  7942  tz7.44-2  8043  fvdiagfn  8455  resixpfo  8500  fival  8876  cantnfp1lem1  9141  cantnfp1lem2  9142  cantnfp1lem3  9143  wemapwe  9160  rankvalb  9226  djulcl  9339  djuss  9349  1stinl  9356  2ndinl  9357  1stinr  9358  2ndinr  9359  fin23lem27  9750  isf34lem1  9794  canthp1lem2  10075  wuncval  10164  climrlim2  14904  summolem3  15071  prodmolem3  15287  iprodmul  15357  lcmfval  15965  iserodd  16172  mreacs  16929  isofval  17027  isofn  17045  cicfval  17067  initoval  17257  termoval  17258  zerooval  17259  pwsco1mhm  17996  pwsco2mhm  17997  vrmdfval  18021  galactghm  18532  symgfixfolem1  18566  pmtrval  18579  pmtrfv  18580  pmtrdifwrdellem3  18611  gsummhm2  19059  gsummpt1n0  19085  dprdfid  19139  lspval  19747  aspval  20102  evlslem3  20293  coe1tmfv1  20442  coe1tmfv2  20443  uvcval  20929  mat1rhmval  21088  scmatrhmval  21136  marepvval  21176  mply1topmatval  21412  mp2pm2mplem1  21414  chfacfscmulgsum  21468  chfacfpmmulgsum  21472  tgval  21563  ntrval  21644  clsval  21645  opncldf2  21693  neival  21710  lpval  21747  1stcfb  22053  cnmpt11  22271  cnmpt21  22279  cnmptkp  22288  cnmptk1p  22293  ustval  22811  iunmbl  24154  cnmptlimc  24488  limccnp  24489  limcco  24491  coe1termlem  24848  coe1term  24849  ulmval  24968  pserulm  25010  efgh  25125  rlimcnp  25543  xrlimcnp  25546  dchrelbasd  25815  gausslemma2dlem4  25945  2lgslem1b  25968  tgjustr  26260  mirval  26441  midf  26562  ismidb  26564  lmif  26571  islmib  26573  wksfval  27391  crctcshwlkn0lem2  27589  crctcshwlkn0lem3  27590  wwlks  27613  wlkiswwlks2lem2  27648  wlkswwlksf1o  27657  clwwlk  27761  clwlkclwwlkf1  27788  numclwlk2lem2fv  28157  spanval  29110  fsuppcurry1  30461  fsuppcurry2  30462  fzto1stfv1  30743  tocycval  30750  prmidlval  30954  indv  31271  esumcvg  31345  omsval  31551  eulerpartlemgvv  31634  cndprobval  31691  reprval  31881  hgt750lemb  31927  satfvsuc  32608  sat1el2xp  32626  fmlasuc0  32631  climlec3  32965  madeval  33289  fwddifval  33623  knoppcnlem1  33832  knoppcnlem9  33840  unbdqndv2lem2  33849  knoppndvlem4  33854  knoppndvlem6  33856  bj-diagval  34469  bj-endval  34599  heiborlem4  35107  heiborlem6  35109  pclvalN  37041  frlmsnic  39169  rabdiophlem2  39419  fphpdo  39434  monotoddzz  39560  dnnumch3lem  39666  pwssplit4  39709  hbtlem1  39743  rgspnval  39788  eliunov2  40044  fvmptiunrelexplb0d  40049  fvmptiunrelexplb1d  40051  dssmapfvd  40383  wessf1ornlem  41465  projf1o  41479  fmuldfeq  41884  clim1fr1  41902  mullimcf  41924  sumnnodd  41931  expfac  41958  fnlimfv  41964  fnlimfvre2  41978  fnlimabslt  41980  limsuplt2  42054  liminfval  42060  limsupge  42062  cncfshift  42177  cncfiooicclem1  42196  fprodsubrecnncnvlem  42211  fprodaddrecnncnvlem  42213  ioodvbdlimc1lem1  42236  ioodvbdlimc1lem2  42237  dvnmul  42248  dvnprodlem1  42251  dvnprodlem2  42252  dvnprodlem3  42253  itgsinexp  42260  stoweidlem7  42312  stoweidlem17  42322  stoweidlem26  42331  stoweidlem30  42335  stoweidlem31  42336  stoweidlem32  42337  stoweidlem34  42339  wallispilem4  42373  wallispi  42375  stirlinglem3  42381  stirlinglem5  42383  stirlinglem7  42385  stirlinglem10  42388  dirkercncflem2  42409  etransclem1  42540  etransclem12  42551  etransclem27  42566  etransclem46  42585  etransclem48  42587  sge0snmptf  42739  nnfoctbdjlem  42757  psmeasurelem  42772  psmeasure  42773  meaiuninclem  42782  meaiininclem  42788  carageniuncllem1  42823  carageniuncllem2  42824  caratheodorylem1  42828  0ome  42831  vonval  42842  ovnval  42843  ovnval2b  42854  hoiprodcl2  42857  ovnlecvr  42860  ovncvrrp  42866  ovnsubaddlem1  42872  hsphoif  42878  hoidmvval  42879  hsphoival  42881  ovnhoilem1  42903  hoidifhspval  42910  hspval  42911  ovncvr2  42913  hspmbllem2  42929  ovnsubadd2lem  42947  vonioolem2  42983  vonicclem2  42986  issmflem  43024  smflimsuplem1  43114  smflimsuplem5  43118  smflimsuplem7  43120  fvmptrabdm  43512  sprsymrelfv  43676  prproropf1olem4  43688  fmtno  43711  prmdvdsfmtnof1  43769  upwlksfval  44030  uspgrsprfv  44040  assintopval  44132  lincop  44483  linc1  44500  lincext3  44531  el0ldep  44541  lincresunit2  44553  lincresunit3lem1  44554  blenval  44651  digfval  44677  lines  44738  spheres  44753