Theorem fvmptd3 6973

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

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

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-iota 6456  df-fun 6502  df-fv 6508

This theorem is referenced by:  mptmpoopabbrd  8034  mptmpoopabbrdOLD  8035  undefval  8228  tz7.44-2  8348  fsetfocdm  8810  fvdiagfn  8841  resixpfo  8886  fival  9327  cantnfp1lem1  9599  cantnfp1lem2  9600  cantnfp1lem3  9601  wemapwe  9618  rankvalb  9721  djulcl  9834  djuss  9844  1stinl  9851  2ndinl  9852  1stinr  9853  2ndinr  9854  fin23lem27  10250  isf34lem1  10294  canthp1lem2  10576  wuncval  10665  climrlim2  15482  summolem3  15649  prodmolem3  15868  iprodmul  15938  lcmfval  16560  iserodd  16775  mreacs  17593  isofval  17693  isofn  17711  cicfval  17733  initoval  17929  termoval  17930  zerooval  17931  pwsco1mhm  18769  pwsco2mhm  18770  vrmdfval  18793  ghmqusnsglem1  19221  ghmquskerlem1  19224  galactghm  19345  symgfixfolem1  19379  pmtrval  19392  pmtrfv  19393  pmtrdifwrdellem3  19424  gsummhm2  19880  gsummpt1n0  19906  dprdfid  19960  rgspnval  20557  lspval  20938  uvcval  21752  aspval  21840  evlslem3  22047  evlsvvval  22060  psdmplcl  22117  psdadd  22118  psdmul  22121  psdmvr  22124  coe1tmfv1  22228  coe1tmfv2  22229  evls1maprhm  22332  evls1maplmhm  22333  rhmmpl  22339  rhmply1vr1  22343  rhmply1vsca  22344  mat1rhmval  22435  scmatrhmval  22483  marepvval  22523  mply1topmatval  22760  mp2pm2mplem1  22762  chfacfscmulgsum  22816  chfacfpmmulgsum  22820  tgval  22911  ntrval  22992  clsval  22993  opncldf2  23041  neival  23058  lpval  23095  1stcfb  23401  cnmpt11  23619  cnmpt21  23627  cnmptkp  23636  cnmptk1p  23641  ustval  24159  iunmbl  25522  cnmptlimc  25859  limccnp  25860  limcco  25862  coe1termlem  26231  coe1term  26232  ulmval  26357  pserulm  26399  efgh  26518  rlimcnp  26943  xrlimcnp  26946  dchrelbasd  27218  gausslemma2dlem4  27348  2lgslem1b  27371  madeval  27840  abssval  28247  tgjustr  28558  mirval  28739  midf  28860  ismidb  28862  lmif  28869  islmib  28871  wksfval  29695  crctcshwlkn0lem2  29896  crctcshwlkn0lem3  29897  wwlks  29920  wlkiswwlks2lem2  29955  wlkswwlksf1o  29964  clwwlk  30070  clwlkclwwlkf1  30097  numclwlk2lem2fv  30465  spanval  31420  fsuppcurry1  32813  fsuppcurry2  32814  indv  32941  mndlactf1  33118  mndlactfo  33119  mndractf1  33120  mndractfo  33121  mndlactf1o  33122  mndractf1o  33123  gsummulsubdishift1s  33163  gsummulsubdishift2s  33164  gsumwrd2dccat  33171  fzto1stfv1  33194  tocycval  33201  fxpsubm  33265  fxpsubg  33266  fxpsubrg  33267  fxpsdrg  33268  elrgspnlem1  33335  elrgspnlem2  33336  elrgspnsubrunlem2  33341  rlocf1  33366  qusrn  33501  elrspunidl  33520  elrspunsn  33521  prmidlval  33529  rprmval  33608  zringfrac  33646  ply1gsumz  33691  r1plmhm  33702  extvfvcl  33712  mplvrpmrhm  33723  psrmonmul2  33727  psrmonprod  33728  esplyfvaln  33750  vietadeg1  33754  ply1degltdimlem  33799  lactlmhm  33811  evls1fldgencl  33847  fldextrspunlsplem  33850  fldextrspunlsp  33851  ply1annidllem  33878  algextdeglem7  33900  rhmpreimacnlem  34061  esumcvg  34263  omsval  34470  eulerpartlemgvv  34553  cndprobval  34610  reprval  34787  hgt750lemb  34833  fineqvnttrclselem2  35297  fineqvnttrclselem3  35298  fineqvnttrclse  35299  satfvsuc  35574  sat1el2xp  35592  fmlasuc0  35597  climlec3  35947  fwddifval  36375  knoppcnlem1  36712  knoppcnlem9  36720  unbdqndv2lem2  36729  knoppndvlem4  36734  knoppndvlem6  36736  bj-diagval  37426  bj-endval  37567  heiborlem4  38062  heiborlem6  38064  pclvalN  40263  frlmsnic  42907  rhmpsr  42917  mplmapghm  42919  evlsbagval  42924  evlsmaprhm  42928  evlsevl  42929  selvvvval  42940  evlselv  42942  mhphflem  42951  prjspnfv01  42979  prjspner01  42980  prjspner1  42981  rabdiophlem2  43156  fphpdo  43171  monotoddzz  43297  dnnumch3lem  43400  pwssplit4  43443  hbtlem1  43477  eliunov2  44032  fvmptiunrelexplb0d  44037  fvmptiunrelexplb1d  44039  dssmapfvd  44370  wessf1ornlem  45541  projf1o  45552  fmuldfeq  45940  clim1fr1  45958  mullimcf  45980  sumnnodd  45987  expfac  46012  fnlimfv  46018  fnlimfvre2  46032  fnlimabslt  46034  limsuplt2  46108  liminfval  46114  limsupge  46116  cncfshift  46229  cncfiooicclem1  46248  fprodsubrecnncnvlem  46262  fprodaddrecnncnvlem  46264  ioodvbdlimc1lem1  46286  ioodvbdlimc1lem2  46287  dvnmul  46298  dvnprodlem1  46301  dvnprodlem2  46302  dvnprodlem3  46303  itgsinexp  46310  stoweidlem7  46362  stoweidlem17  46372  stoweidlem26  46381  stoweidlem30  46385  stoweidlem31  46386  stoweidlem32  46387  stoweidlem34  46389  wallispilem4  46423  wallispi  46425  stirlinglem3  46431  stirlinglem5  46433  stirlinglem7  46435  stirlinglem10  46438  dirkercncflem2  46459  etransclem1  46590  etransclem12  46601  etransclem27  46616  etransclem46  46635  etransclem48  46637  sge0snmptf  46792  nnfoctbdjlem  46810  psmeasurelem  46825  psmeasure  46826  meaiuninclem  46835  meaiininclem  46841  carageniuncllem1  46876  carageniuncllem2  46877  caratheodorylem1  46881  0ome  46884  vonval  46895  ovnval  46896  ovnval2b  46907  hoiprodcl2  46910  ovnlecvr  46913  ovncvrrp  46919  ovnsubaddlem1  46925  hsphoif  46931  hoidmvval  46932  hsphoival  46934  ovnhoilem1  46956  hoidifhspval  46963  hspval  46964  ovncvr2  46966  hspmbllem2  46982  ovnsubadd2lem  47000  vonioolem2  47036  vonicclem2  47039  issmflem  47082  smflimsuplem1  47175  smflimsuplem5  47179  smflimsuplem7  47181  fvmptrabdm  47650  sprsymrelfv  47851  prproropf1olem4  47863  fmtno  47886  prmdvdsfmtnof1  47944  upwlksfval  48492  uspgrsprfv  48502  assintopval  48562  lincop  48765  linc1  48782  lincext3  48813  el0ldep  48823  lincresunit2  48835  lincresunit3lem1  48836  blenval  48928  digfval  48954  itcoval  49018  ackval0012  49046  ackval1012  49047  ackval2012  49048  ackval3012  49049  lines  49088  spheres  49103  invfn  49386  fucoid  49704