Theorem mpteq2ia 5193

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 5191	. 2 ⊢ (⊤ → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))
4	3	mptru 1548	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4   = wceq 1541  ⊤wtru 1542   ∈ wcel 2113   ↦ cmpt 5179

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 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-opab 5161  df-mpt 5180

This theorem is referenced by:  mpteq2i  5194  partfun  6639  feqresmpt  6903  elfvmptrab  6970  fmptap  7116  offres  7927  resixpfo  8874  dfoi  9416  cantnflem1d  9597  cantnflem1  9598  dfceil2  13759  dfid5  14950  dfid6  14951  cnrecnv  15088  ackbijnn  15751  harmonic  15782  ege2le3  16013  eirrlem  16129  prmrec  16850  imasdsval2  17437  dfinito2  17927  dftermo2  17928  dfinito3  17929  dftermo3  17930  smndex1iidm  18826  smndex2dlinvh  18842  cayleylem1  19341  pmtrprfval  19416  gsumzsplit  19856  gsum2dlem2  19900  dmdprdsplitlem  19968  frlmip  21733  coe1sclmul  22224  coe1sclmul2  22226  mdetunilem9  22564  leordtvallem1  23154  leordtvallem2  23155  txkgen  23596  cnmpt1st  23612  cnmpt2nd  23613  tmdgsum  24039  tsmssplit  24096  cnfldnm  24722  expcn  24819  expcnOLD  24821  pcorev2  24984  pi1xfrcnv  25013  rrxip  25346  mbfi1flim  25680  itg2uba  25700  itg2cnlem1  25718  itg2cnlem2  25719  itgitg2  25764  itgss3  25772  itgless  25774  ibladdlem  25777  itgaddlem1  25780  iblabslem  25785  itggt0  25801  itgcn  25802  limcdif  25833  limcres  25843  cnplimc  25844  dvcobr  25905  dvcobrOLD  25906  dvexp  25913  dveflem  25939  dvef  25940  dvlip  25954  dvlipcn  25955  lhop  25977  tdeglem2  26022  plyid  26170  coeidp  26225  dgrid  26226  pserdvlem2  26394  abelth  26407  dvrelog  26602  logcn  26612  dvlog  26616  advlog  26619  advlogexp  26620  logtayl  26625  logccv  26628  dvcxp1  26705  dvsqrt  26707  dvcncxp1  26708  dvcnsqrt  26709  resqrtcn  26715  loglesqrt  26727  logblog  26758  dvatan  26901  leibpilem2  26907  leibpi  26908  efrlim  26935  efrlimOLD  26936  sqrtlim  26939  amgmlem  26956  emcllem5  26966  lgamgulmlem2  26996  lgam1  27030  chtublem  27178  logfacrlim2  27193  bposlem6  27256  chto1lb  27445  vmadivsum  27449  dchrvmasumlema  27467  mulogsumlem  27498  logdivsum  27500  logsqvma2  27510  log2sumbnd  27511  selberglem1  27512  selberglem3  27514  selberg  27515  selberg2lem  27517  selberg2  27518  pntrmax  27531  pntrsumo1  27532  selbergr  27535  selbergs  27541  pnt2  27580  pnt  27581  ostth2  27604  ostth  27606  hilnormi  31238  bra0  32025  partfun2  32755  zrhre  34176  qqhre  34177  eulerpartgbij  34529  plymulx  34705  elmrsubrn  35714  faclim  35940  ptrest  37820  poimirlem19  37840  poimirlem20  37841  poimirlem30  37851  ovoliunnfl  37863  voliunnfl  37865  mbfposadd  37868  dvtan  37871  itg2addnclem  37872  ibladdnclem  37877  itgaddnclem1  37879  iblabsnclem  37884  itggt0cn  37891  ftc1anclem4  37897  ftc1anclem5  37898  ftc1anclem6  37899  ftc1anclem7  37900  ftc1anclem8  37901  dvasin  37905  dvacos  37906  areacirclem1  37909  dfadjliftmap2  38632  dfblockliftmap2  38635  aks6d1c1p5  42366  redvmptabs  42615  readvrec2  42616  readvrec  42617  readvcot  42619  arearect  43457  areaquad  43458  cantnfresb  43566  mptrcllem  43854  dfrcl2  43915  dfrcl3  43916  dftrcl3  43961  dfrtrcl3  43974  dfrtrcl4  43979  lhe4.4ex1a  44570  binomcxplemrat  44591  rnsnf  45428  feqresmptf  45475  limsupresre  45940  limsupvaluzmpt  45961  limsup10ex  46017  liminf10ex  46018  dvnprodlem1  46190  itgsin0pilem1  46194  wallispilem4  46312  wallispi2  46317  stirlinglem1  46318  stirlinglem3  46320  dirkercncflem2  46348  fourierdlem48  46398  fourierdlem49  46399  fourierdlem56  46406  fourierdlem57  46407  fourierdlem58  46408  fourierdlem62  46412  fourierdlem107  46457  fouriersw  46475  etransclem46  46524  sge0tsms  46624  sge0less  46636  sge0iun  46663  meadjun  46706  ovn02  46812  hoidmv1le  46838  hspmbllem2  46871  smflimsuplem3  47066  ackval1  48927  ackval2  48928  ackval3  48929  dftermo4  49747