Theorem fvmptd3 6810

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114   ↦ cmpt 5120  ‘cfv 6349

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2711  ax-sep 5177  ax-nul 5184  ax-pr 5306

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2541  df-eu 2571  df-clab 2718  df-cleq 2731  df-clel 2812  df-nfc 2882  df-ral 3059  df-rex 3060  df-v 3402  df-sbc 3686  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4222  df-if 4425  df-sn 4527  df-pr 4529  df-op 4533  df-uni 4807  df-br 5041  df-opab 5103  df-mpt 5121  df-id 5439  df-xp 5541  df-rel 5542  df-cnv 5543  df-co 5544  df-dm 5545  df-iota 6307  df-fun 6351  df-fv 6357

This theorem is referenced by:  mptmpoopabbrd  7816  undefval  7983  tz7.44-2  8084  fvdiagfn  8513  resixpfo  8558  fival  8961  cantnfp1lem1  9226  cantnfp1lem2  9227  cantnfp1lem3  9228  wemapwe  9245  rankvalb  9311  djulcl  9424  djuss  9434  1stinl  9441  2ndinl  9442  1stinr  9443  2ndinr  9444  fin23lem27  9840  isf34lem1  9884  canthp1lem2  10165  wuncval  10254  climrlim2  15006  summolem3  15176  prodmolem3  15391  iprodmul  15461  lcmfval  16074  iserodd  16284  mreacs  17044  isofval  17144  isofn  17162  cicfval  17184  initoval  17377  termoval  17378  zerooval  17379  pwsco1mhm  18124  pwsco2mhm  18125  vrmdfval  18149  galactghm  18662  symgfixfolem1  18696  pmtrval  18709  pmtrfv  18710  pmtrdifwrdellem3  18741  gsummhm2  19190  gsummpt1n0  19216  dprdfid  19270  lspval  19878  uvcval  20613  aspval  20698  evlslem3  20906  coe1tmfv1  21061  coe1tmfv2  21062  mat1rhmval  21242  scmatrhmval  21290  marepvval  21330  mply1topmatval  21567  mp2pm2mplem1  21569  chfacfscmulgsum  21623  chfacfpmmulgsum  21627  tgval  21718  ntrval  21799  clsval  21800  opncldf2  21848  neival  21865  lpval  21902  1stcfb  22208  cnmpt11  22426  cnmpt21  22434  cnmptkp  22443  cnmptk1p  22448  ustval  22966  iunmbl  24317  cnmptlimc  24654  limccnp  24655  limcco  24657  coe1termlem  25019  coe1term  25020  ulmval  25139  pserulm  25181  efgh  25297  rlimcnp  25715  xrlimcnp  25718  dchrelbasd  25987  gausslemma2dlem4  26117  2lgslem1b  26140  tgjustr  26432  mirval  26613  midf  26734  ismidb  26736  lmif  26743  islmib  26745  wksfval  27563  crctcshwlkn0lem2  27761  crctcshwlkn0lem3  27762  wwlks  27785  wlkiswwlks2lem2  27820  wlkswwlksf1o  27829  clwwlk  27932  clwlkclwwlkf1  27959  numclwlk2lem2fv  28327  spanval  29280  fsuppcurry1  30647  fsuppcurry2  30648  fzto1stfv1  30957  tocycval  30964  elrspunidl  31190  prmidlval  31196  rprmval  31248  rhmpreimacnlem  31418  indv  31562  esumcvg  31636  omsval  31842  eulerpartlemgvv  31925  cndprobval  31982  reprval  32172  hgt750lemb  32218  satfvsuc  32906  sat1el2xp  32924  fmlasuc0  32929  climlec3  33284  madeval  33691  fwddifval  34119  knoppcnlem1  34328  knoppcnlem9  34336  unbdqndv2lem2  34345  knoppndvlem4  34350  knoppndvlem6  34352  bj-diagval  34998  bj-endval  35138  heiborlem4  35627  heiborlem6  35629  pclvalN  37559  frlmsnic  39884  evlsbagval  39894  mhphflem  39903  prjspnfv01  40078  prjspner01  40079  prjspner1  40080  rabdiophlem2  40236  fphpdo  40251  monotoddzz  40377  dnnumch3lem  40483  pwssplit4  40526  hbtlem1  40560  rgspnval  40605  eliunov2  40873  fvmptiunrelexplb0d  40878  fvmptiunrelexplb1d  40880  dssmapfvd  41211  wessf1ornlem  42300  projf1o  42314  fmuldfeq  42706  clim1fr1  42724  mullimcf  42746  sumnnodd  42753  expfac  42780  fnlimfv  42786  fnlimfvre2  42800  fnlimabslt  42802  limsuplt2  42876  liminfval  42882  limsupge  42884  cncfshift  42997  cncfiooicclem1  43016  fprodsubrecnncnvlem  43030  fprodaddrecnncnvlem  43032  ioodvbdlimc1lem1  43054  ioodvbdlimc1lem2  43055  dvnmul  43066  dvnprodlem1  43069  dvnprodlem2  43070  dvnprodlem3  43071  itgsinexp  43078  stoweidlem7  43130  stoweidlem17  43140  stoweidlem26  43149  stoweidlem30  43153  stoweidlem31  43154  stoweidlem32  43155  stoweidlem34  43157  wallispilem4  43191  wallispi  43193  stirlinglem3  43199  stirlinglem5  43201  stirlinglem7  43203  stirlinglem10  43206  dirkercncflem2  43227  etransclem1  43358  etransclem12  43369  etransclem27  43384  etransclem46  43403  etransclem48  43405  sge0snmptf  43557  nnfoctbdjlem  43575  psmeasurelem  43590  psmeasure  43591  meaiuninclem  43600  meaiininclem  43606  carageniuncllem1  43641  carageniuncllem2  43642  caratheodorylem1  43646  0ome  43649  vonval  43660  ovnval  43661  ovnval2b  43672  hoiprodcl2  43675  ovnlecvr  43678  ovncvrrp  43684  ovnsubaddlem1  43690  hsphoif  43696  hoidmvval  43697  hsphoival  43699  ovnhoilem1  43721  hoidifhspval  43728  hspval  43729  ovncvr2  43731  hspmbllem2  43747  ovnsubadd2lem  43765  vonioolem2  43801  vonicclem2  43804  issmflem  43842  smflimsuplem1  43932  smflimsuplem5  43936  smflimsuplem7  43938  fvmptrabdm  44365  sprsymrelfv  44527  prproropf1olem4  44539  fmtno  44562  prmdvdsfmtnof1  44620  upwlksfval  44878  uspgrsprfv  44888  assintopval  44980  lincop  45330  linc1  45347  lincext3  45378  el0ldep  45388  lincresunit2  45400  lincresunit3lem1  45401  blenval  45498  digfval  45524  itcoval  45588  ackval0012  45616  ackval1012  45617  ackval2012  45618  ackval3012  45619  lines  45658  spheres  45673