Theorem fvmptd3 6952

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111   ↦ cmpt 5172  ‘cfv 6481

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-mpt 5173  df-id 5511  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-iota 6437  df-fun 6483  df-fv 6489

This theorem is referenced by:  mptmpoopabbrd  8012  mptmpoopabbrdOLD  8013  undefval  8206  tz7.44-2  8326  fsetfocdm  8785  fvdiagfn  8815  resixpfo  8860  fival  9296  cantnfp1lem1  9568  cantnfp1lem2  9569  cantnfp1lem3  9570  wemapwe  9587  rankvalb  9690  djulcl  9803  djuss  9813  1stinl  9820  2ndinl  9821  1stinr  9822  2ndinr  9823  fin23lem27  10219  isf34lem1  10263  canthp1lem2  10544  wuncval  10633  climrlim2  15454  summolem3  15621  prodmolem3  15840  iprodmul  15910  lcmfval  16532  iserodd  16747  mreacs  17564  isofval  17664  isofn  17682  cicfval  17704  initoval  17900  termoval  17901  zerooval  17902  pwsco1mhm  18740  pwsco2mhm  18741  vrmdfval  18764  ghmqusnsglem1  19193  ghmquskerlem1  19196  galactghm  19317  symgfixfolem1  19351  pmtrval  19364  pmtrfv  19365  pmtrdifwrdellem3  19396  gsummhm2  19852  gsummpt1n0  19878  dprdfid  19932  rgspnval  20528  lspval  20909  uvcval  21723  aspval  21811  evlslem3  22016  psdmplcl  22078  psdadd  22079  psdmul  22082  psdmvr  22085  coe1tmfv1  22189  coe1tmfv2  22190  evls1maprhm  22292  evls1maplmhm  22293  rhmmpl  22299  rhmply1vr1  22303  rhmply1vsca  22304  mat1rhmval  22395  scmatrhmval  22443  marepvval  22483  mply1topmatval  22720  mp2pm2mplem1  22722  chfacfscmulgsum  22776  chfacfpmmulgsum  22780  tgval  22871  ntrval  22952  clsval  22953  opncldf2  23001  neival  23018  lpval  23055  1stcfb  23361  cnmpt11  23579  cnmpt21  23587  cnmptkp  23596  cnmptk1p  23601  ustval  24119  iunmbl  25482  cnmptlimc  25819  limccnp  25820  limcco  25822  coe1termlem  26191  coe1term  26192  ulmval  26317  pserulm  26359  efgh  26478  rlimcnp  26903  xrlimcnp  26906  dchrelbasd  27178  gausslemma2dlem4  27308  2lgslem1b  27331  madeval  27794  abssval  28178  tgjustr  28453  mirval  28634  midf  28755  ismidb  28757  lmif  28764  islmib  28766  wksfval  29589  crctcshwlkn0lem2  29790  crctcshwlkn0lem3  29791  wwlks  29814  wlkiswwlks2lem2  29849  wlkswwlksf1o  29858  clwwlk  29961  clwlkclwwlkf1  29988  numclwlk2lem2fv  30356  spanval  31311  fsuppcurry1  32705  fsuppcurry2  32706  indv  32831  mndlactf1  33005  mndlactfo  33006  mndractf1  33007  mndractfo  33008  mndlactf1o  33009  mndractf1o  33010  gsumwrd2dccat  33045  fzto1stfv1  33068  tocycval  33075  fxpsubm  33139  fxpsubg  33140  fxpsubrg  33141  fxpsdrg  33142  elrgspnlem1  33207  elrgspnlem2  33208  elrgspnsubrunlem2  33213  rlocf1  33238  qusrn  33372  elrspunidl  33391  elrspunsn  33392  prmidlval  33400  rprmval  33479  zringfrac  33517  ply1gsumz  33557  r1plmhm  33568  mplvrpmrhm  33575  ply1degltdimlem  33633  lactlmhm  33645  evls1fldgencl  33681  fldextrspunlsplem  33684  fldextrspunlsp  33685  ply1annidllem  33712  algextdeglem7  33734  rhmpreimacnlem  33895  esumcvg  34097  omsval  34304  eulerpartlemgvv  34387  cndprobval  34444  reprval  34621  hgt750lemb  34667  fineqvnttrclselem2  35140  fineqvnttrclselem3  35141  fineqvnttrclse  35142  satfvsuc  35403  sat1el2xp  35421  fmlasuc0  35426  climlec3  35776  fwddifval  36202  knoppcnlem1  36533  knoppcnlem9  36541  unbdqndv2lem2  36550  knoppndvlem4  36555  knoppndvlem6  36557  bj-diagval  37214  bj-endval  37355  heiborlem4  37860  heiborlem6  37862  pclvalN  39935  frlmsnic  42579  rhmpsr  42591  mplmapghm  42595  evlsvvval  42602  evlsbagval  42605  evlsmaprhm  42609  evlsevl  42610  selvvvval  42624  evlselv  42626  mhphflem  42635  prjspnfv01  42663  prjspner01  42664  prjspner1  42665  rabdiophlem2  42841  fphpdo  42856  monotoddzz  42982  dnnumch3lem  43085  pwssplit4  43128  hbtlem1  43162  eliunov2  43718  fvmptiunrelexplb0d  43723  fvmptiunrelexplb1d  43725  dssmapfvd  44056  wessf1ornlem  45228  projf1o  45240  fmuldfeq  45629  clim1fr1  45647  mullimcf  45669  sumnnodd  45676  expfac  45701  fnlimfv  45707  fnlimfvre2  45721  fnlimabslt  45723  limsuplt2  45797  liminfval  45803  limsupge  45805  cncfshift  45918  cncfiooicclem1  45937  fprodsubrecnncnvlem  45951  fprodaddrecnncnvlem  45953  ioodvbdlimc1lem1  45975  ioodvbdlimc1lem2  45976  dvnmul  45987  dvnprodlem1  45990  dvnprodlem2  45991  dvnprodlem3  45992  itgsinexp  45999  stoweidlem7  46051  stoweidlem17  46061  stoweidlem26  46070  stoweidlem30  46074  stoweidlem31  46075  stoweidlem32  46076  stoweidlem34  46078  wallispilem4  46112  wallispi  46114  stirlinglem3  46120  stirlinglem5  46122  stirlinglem7  46124  stirlinglem10  46127  dirkercncflem2  46148  etransclem1  46279  etransclem12  46290  etransclem27  46305  etransclem46  46324  etransclem48  46326  sge0snmptf  46481  nnfoctbdjlem  46499  psmeasurelem  46514  psmeasure  46515  meaiuninclem  46524  meaiininclem  46530  carageniuncllem1  46565  carageniuncllem2  46566  caratheodorylem1  46570  0ome  46573  vonval  46584  ovnval  46585  ovnval2b  46596  hoiprodcl2  46599  ovnlecvr  46602  ovncvrrp  46608  ovnsubaddlem1  46614  hsphoif  46620  hoidmvval  46621  hsphoival  46623  ovnhoilem1  46645  hoidifhspval  46652  hspval  46653  ovncvr2  46655  hspmbllem2  46671  ovnsubadd2lem  46689  vonioolem2  46725  vonicclem2  46728  issmflem  46771  smflimsuplem1  46864  smflimsuplem5  46868  smflimsuplem7  46870  fvmptrabdm  47330  sprsymrelfv  47531  prproropf1olem4  47543  fmtno  47566  prmdvdsfmtnof1  47624  upwlksfval  48172  uspgrsprfv  48182  assintopval  48242  lincop  48446  linc1  48463  lincext3  48494  el0ldep  48504  lincresunit2  48516  lincresunit3lem1  48517  blenval  48609  digfval  48635  itcoval  48699  ackval0012  48727  ackval1012  48728  ackval2012  48729  ackval3012  48730  lines  48769  spheres  48784  invfn  49068  fucoid  49386