Theorem mpteq2ia 5250

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

Syntax hints:   → wi 4   = wceq 1539  ⊤wtru 1540   ∈ wcel 2104   ↦ cmpt 5230

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-opab 5210  df-mpt 5231

This theorem is referenced by:  mpteq2i  5252  partfun  6696  feqresmpt  6960  elfvmptrab  7025  fmptap  7169  offres  7972  resixpfo  8932  dfoi  9508  cantnflem1d  9685  cantnflem1  9686  dfceil2  13808  dfid5  14978  dfid6  14979  cnrecnv  15116  ackbijnn  15778  harmonic  15809  ege2le3  16037  eirrlem  16151  prmrec  16859  imasdsval2  17466  dfinito2  17957  dftermo2  17958  dfinito3  17959  dftermo3  17960  smndex1iidm  18818  smndex2dlinvh  18834  cayleylem1  19321  pmtrprfval  19396  gsumzsplit  19836  gsum2dlem2  19880  dmdprdsplitlem  19948  frlmip  21552  coe1sclmul  22024  coe1sclmul2  22026  mdetunilem9  22342  leordtvallem1  22934  leordtvallem2  22935  txkgen  23376  cnmpt1st  23392  cnmpt2nd  23393  tmdgsum  23819  tsmssplit  23876  cnfldnm  24515  expcn  24610  expcnOLD  24612  pcorev2  24775  pi1xfrcnv  24804  rrxip  25138  mbfi1flim  25473  itg2uba  25493  itg2cnlem1  25511  itg2cnlem2  25512  itgitg2  25556  itgss3  25564  itgless  25566  ibladdlem  25569  itgaddlem1  25572  iblabslem  25577  itggt0  25593  itgcn  25594  limcdif  25625  limcres  25635  cnplimc  25636  dvcobr  25697  dvcobrOLD  25698  dvexp  25705  dveflem  25731  dvef  25732  dvlip  25745  dvlipcn  25746  lhop  25768  tdeglem2  25814  plyid  25958  coeidp  26013  dgrid  26014  pserdvlem2  26176  abelth  26189  dvrelog  26381  logcn  26391  dvlog  26395  advlog  26398  advlogexp  26399  logtayl  26404  logccv  26407  dvcxp1  26484  dvsqrt  26486  dvcncxp1  26487  dvcnsqrt  26488  resqrtcn  26493  loglesqrt  26502  logblog  26533  dvatan  26676  leibpilem2  26682  leibpi  26683  efrlim  26710  sqrtlim  26713  amgmlem  26730  emcllem5  26740  lgamgulmlem2  26770  lgam1  26804  chtublem  26950  logfacrlim2  26965  bposlem6  27028  chto1lb  27217  vmadivsum  27221  dchrvmasumlema  27239  mulogsumlem  27270  logdivsum  27272  logsqvma2  27282  log2sumbnd  27283  selberglem1  27284  selberglem3  27286  selberg  27287  selberg2lem  27289  selberg2  27290  pntrmax  27303  pntrsumo1  27304  selbergr  27307  selbergs  27313  pnt2  27352  pnt  27353  ostth2  27376  ostth  27378  hilnormi  30683  bra0  31470  zrhre  33297  qqhre  33298  eulerpartgbij  33669  plymulx  33857  elmrsubrn  34809  faclim  35020  ptrest  36790  poimirlem19  36810  poimirlem20  36811  poimirlem30  36821  ovoliunnfl  36833  voliunnfl  36835  mbfposadd  36838  dvtan  36841  itg2addnclem  36842  ibladdnclem  36847  itgaddnclem1  36849  iblabsnclem  36854  itggt0cn  36861  ftc1anclem4  36867  ftc1anclem5  36868  ftc1anclem6  36869  ftc1anclem7  36870  ftc1anclem8  36871  dvasin  36875  dvacos  36876  areacirclem1  36879  arearect  42266  areaquad  42267  cantnfresb  42376  mptrcllem  42666  dfrcl2  42727  dfrcl3  42728  dftrcl3  42773  dfrtrcl3  42786  dfrtrcl4  42791  lhe4.4ex1a  43390  binomcxplemrat  43411  rnsnf  44181  feqresmptf  44229  limsupresre  44710  limsupvaluzmpt  44731  limsup10ex  44787  liminf10ex  44788  dvnprodlem1  44960  itgsin0pilem1  44964  wallispilem4  45082  wallispi2  45087  stirlinglem1  45088  stirlinglem3  45090  dirkercncflem2  45118  fourierdlem48  45168  fourierdlem49  45169  fourierdlem56  45176  fourierdlem57  45177  fourierdlem58  45178  fourierdlem62  45182  fourierdlem107  45227  fouriersw  45245  etransclem46  45294  sge0tsms  45394  sge0less  45406  sge0iun  45433  meadjun  45476  ovn02  45582  hoidmv1le  45608  hspmbllem2  45641  smflimsuplem3  45836  ackval1  47454  ackval2  47455  ackval3  47456