Theorem mpteq2ia 5251

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 483	. . 3 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
3	2	mpteq2dva 5248	. 2 ⊢ (⊤ → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))
4	3	mptru 1549	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-opab 5211  df-mpt 5232

This theorem is referenced by:  mpteq2i  5253  partfun  6695  feqresmpt  6959  elfvmptrab  7024  fmptap  7165  offres  7967  resixpfo  8927  dfoi  9503  cantnflem1d  9680  cantnflem1  9681  dfceil2  13801  dfid5  14971  dfid6  14972  cnrecnv  15109  ackbijnn  15771  harmonic  15802  ege2le3  16030  eirrlem  16144  prmrec  16852  imasdsval2  17459  dfinito2  17950  dftermo2  17951  dfinito3  17952  dftermo3  17953  smndex1iidm  18779  smndex2dlinvh  18795  cayleylem1  19275  pmtrprfval  19350  gsumzsplit  19790  gsum2dlem2  19834  dmdprdsplitlem  19902  frlmip  21325  coe1sclmul  21796  coe1sclmul2  21798  mdetunilem9  22114  leordtvallem1  22706  leordtvallem2  22707  txkgen  23148  cnmpt1st  23164  cnmpt2nd  23165  tmdgsum  23591  tsmssplit  23648  cnfldnm  24287  expcn  24380  pcorev2  24536  pi1xfrcnv  24565  rrxip  24899  mbfi1flim  25233  itg2uba  25253  itg2cnlem1  25271  itg2cnlem2  25272  itgitg2  25316  itgss3  25324  itgless  25326  ibladdlem  25329  itgaddlem1  25332  iblabslem  25337  itggt0  25353  itgcn  25354  limcdif  25385  limcres  25395  cnplimc  25396  dvcobr  25455  dvexp  25462  dveflem  25488  dvef  25489  dvlip  25502  dvlipcn  25503  lhop  25525  tdeglem2  25571  plyid  25715  coeidp  25769  dgrid  25770  pserdvlem2  25932  abelth  25945  dvrelog  26137  logcn  26147  dvlog  26151  advlog  26154  advlogexp  26155  logtayl  26160  logccv  26163  dvcxp1  26238  dvsqrt  26240  dvcncxp1  26241  dvcnsqrt  26242  resqrtcn  26247  loglesqrt  26256  logblog  26287  dvatan  26430  leibpilem2  26436  leibpi  26437  efrlim  26464  sqrtlim  26467  amgmlem  26484  emcllem5  26494  lgamgulmlem2  26524  lgam1  26558  chtublem  26704  logfacrlim2  26719  bposlem6  26782  chto1lb  26971  vmadivsum  26975  dchrvmasumlema  26993  mulogsumlem  27024  logdivsum  27026  logsqvma2  27036  log2sumbnd  27037  selberglem1  27038  selberglem3  27040  selberg  27041  selberg2lem  27043  selberg2  27044  pntrmax  27057  pntrsumo1  27058  selbergr  27061  selbergs  27067  pnt2  27106  pnt  27107  ostth2  27130  ostth  27132  hilnormi  30404  bra0  31191  zrhre  32988  qqhre  32989  eulerpartgbij  33360  plymulx  33548  elmrsubrn  34500  faclim  34705  gg-expcn  35153  gg-dvcobr  35165  ptrest  36476  poimirlem19  36496  poimirlem20  36497  poimirlem30  36507  ovoliunnfl  36519  voliunnfl  36521  mbfposadd  36524  dvtan  36527  itg2addnclem  36528  ibladdnclem  36533  itgaddnclem1  36535  iblabsnclem  36540  itggt0cn  36547  ftc1anclem4  36553  ftc1anclem5  36554  ftc1anclem6  36555  ftc1anclem7  36556  ftc1anclem8  36557  dvasin  36561  dvacos  36562  areacirclem1  36565  arearect  41950  areaquad  41951  cantnfresb  42060  mptrcllem  42350  dfrcl2  42411  dfrcl3  42412  dftrcl3  42457  dfrtrcl3  42470  dfrtrcl4  42475  lhe4.4ex1a  43074  binomcxplemrat  43095  rnsnf  43867  feqresmptf  43917  limsupresre  44399  limsupvaluzmpt  44420  limsup10ex  44476  liminf10ex  44477  dvnprodlem1  44649  itgsin0pilem1  44653  wallispilem4  44771  wallispi2  44776  stirlinglem1  44777  stirlinglem3  44779  dirkercncflem2  44807  fourierdlem48  44857  fourierdlem49  44858  fourierdlem56  44865  fourierdlem57  44866  fourierdlem58  44867  fourierdlem62  44871  fourierdlem107  44916  fouriersw  44934  etransclem46  44983  sge0tsms  45083  sge0less  45095  sge0iun  45122  meadjun  45165  ovn02  45271  hoidmv1le  45297  hspmbllem2  45330  smflimsuplem3  45525  ackval1  47321  ackval2  47322  ackval3  47323