Theorem mpteq2ia 5180

Description: An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) (Proof shortened by SN, 11-Nov-2024.)

Hypothesis

Ref	Expression
mpteq2ia.1	⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶)

Assertion

Ref	Expression
mpteq2ia	⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)

Proof of Theorem mpteq2ia

Step	Hyp	Ref	Expression
1		mpteq2ia.1	. . . 4 ⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶)
2	1	adantl 481	. . 3 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
3	2	mpteq2dva 5178	. 2 ⊢ (⊤ → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))
4	3	mptru 1549	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4   = wceq 1542  ⊤wtru 1543   ∈ wcel 2114   ↦ cmpt 5166

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-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-opab 5148  df-mpt 5167

This theorem is referenced by:  mpteq2i  5181  partfun  6645  feqresmpt  6909  elfvmptrab  6977  fmptap  7125  offres  7936  resixpfo  8884  dfoi  9426  cantnflem1d  9609  cantnflem1  9610  dfceil2  13798  dfid5  14989  dfid6  14990  cnrecnv  15127  ackbijnn  15793  harmonic  15824  ege2le3  16055  eirrlem  16171  prmrec  16893  imasdsval2  17480  dfinito2  17970  dftermo2  17971  dfinito3  17972  dftermo3  17973  smndex1iidm  18869  smndex2dlinvh  18888  cayleylem1  19387  pmtrprfval  19462  gsumzsplit  19902  gsum2dlem2  19946  dmdprdsplitlem  20014  frlmip  21758  coe1sclmul  22247  coe1sclmul2  22249  mdetunilem9  22585  leordtvallem1  23175  leordtvallem2  23176  txkgen  23617  cnmpt1st  23633  cnmpt2nd  23634  tmdgsum  24060  tsmssplit  24117  cnfldnm  24743  expcn  24839  pcorev2  24995  pi1xfrcnv  25024  rrxip  25357  mbfi1flim  25690  itg2uba  25710  itg2cnlem1  25728  itg2cnlem2  25729  itgitg2  25774  itgss3  25782  itgless  25784  ibladdlem  25787  itgaddlem1  25790  iblabslem  25795  itggt0  25811  itgcn  25812  limcdif  25843  limcres  25853  cnplimc  25854  dvcobr  25913  dvexp  25920  dveflem  25946  dvef  25947  dvlip  25960  dvlipcn  25961  lhop  25983  tdeglem2  26026  plyid  26174  coeidp  26228  dgrid  26229  pserdvlem2  26393  abelth  26406  dvrelog  26601  logcn  26611  dvlog  26615  advlog  26618  advlogexp  26619  logtayl  26624  logccv  26627  dvcxp1  26704  dvsqrt  26706  dvcncxp1  26707  dvcnsqrt  26708  resqrtcn  26713  loglesqrt  26725  logblog  26756  dvatan  26899  leibpilem2  26905  leibpi  26906  efrlim  26933  sqrtlim  26936  amgmlem  26953  emcllem5  26963  lgamgulmlem2  26993  lgam1  27027  chtublem  27174  logfacrlim2  27189  bposlem6  27252  chto1lb  27441  vmadivsum  27445  dchrvmasumlema  27463  mulogsumlem  27494  logdivsum  27496  logsqvma2  27506  log2sumbnd  27507  selberglem1  27508  selberglem3  27510  selberg  27511  selberg2lem  27513  selberg2  27514  pntrmax  27527  pntrsumo1  27528  selbergr  27531  selbergs  27537  pnt2  27576  pnt  27577  ostth2  27600  ostth  27602  hilnormi  31234  bra0  32021  partfun2  32749  mplmonprod  33698  zrhre  34163  qqhre  34164  eulerpartgbij  34516  plymulx  34692  elmrsubrn  35702  faclim  35928  ptrest  37940  poimirlem19  37960  poimirlem20  37961  poimirlem30  37971  ovoliunnfl  37983  voliunnfl  37985  mbfposadd  37988  dvtan  37991  itg2addnclem  37992  ibladdnclem  37997  itgaddnclem1  37999  iblabsnclem  38004  itggt0cn  38011  ftc1anclem4  38017  ftc1anclem5  38018  ftc1anclem6  38019  ftc1anclem7  38020  ftc1anclem8  38021  dvasin  38025  dvacos  38026  areacirclem1  38029  dfadjliftmap2  38778  dfblockliftmap2  38782  aks6d1c1p5  42551  redvmptabs  42792  readvrec2  42793  readvrec  42794  readvcot  42796  arearect  43643  areaquad  43644  cantnfresb  43752  mptrcllem  44040  dfrcl2  44101  dfrcl3  44102  dftrcl3  44147  dfrtrcl3  44160  dfrtrcl4  44165  lhe4.4ex1a  44756  binomcxplemrat  44777  rnsnf  45614  feqresmptf  45660  limsupresre  46124  limsupvaluzmpt  46145  limsup10ex  46201  liminf10ex  46202  dvnprodlem1  46374  itgsin0pilem1  46378  wallispilem4  46496  wallispi2  46501  stirlinglem1  46502  stirlinglem3  46504  dirkercncflem2  46532  fourierdlem48  46582  fourierdlem49  46583  fourierdlem56  46590  fourierdlem57  46591  fourierdlem58  46592  fourierdlem62  46596  fourierdlem107  46641  fouriersw  46659  etransclem46  46708  sge0tsms  46808  sge0less  46820  sge0iun  46847  meadjun  46890  ovn02  46996  hoidmv1le  47022  hspmbllem2  47055  smflimsuplem3  47250  indprm  48092  indprmfz  48093  ackval1  49157  ackval2  49158  ackval3  49159  dftermo4  49977